From 8120576e9aa08d2ffea09f42b0c7b3be67e19e4f Mon Sep 17 00:00:00 2001 From: agle Date: Thu, 2 Apr 2026 11:10:57 +1000 Subject: [PATCH] minimal proc extraction --- lib/analysis/irreducible_loops.ml | 7 +- lib/lang/dune | 1 + lib/lang/expr_smt.ml | 51 ++++- lib/lang/procedure.ml | 25 ++- lib/lang/reduction.ml | 0 lib/passes.ml | 18 +- lib/transforms/dune | 3 +- lib/transforms/ssa.ml | 22 +- lib/transforms/verif_smt.ml | 331 ++++++++++++++++++++++++++++++ lib/util/smt.ml | 16 +- 10 files changed, 434 insertions(+), 40 deletions(-) create mode 100644 lib/lang/reduction.ml create mode 100644 lib/transforms/verif_smt.ml diff --git a/lib/analysis/irreducible_loops.ml b/lib/analysis/irreducible_loops.ml index 18d8e823..fa8cb244 100644 --- a/lib/analysis/irreducible_loops.ml +++ b/lib/analysis/irreducible_loops.ml @@ -459,13 +459,12 @@ module ProcIntra = struct let find_edge p src dest : edge = let open Option in - Procedure.blocks_succ p src |> Iter.find_pred (fst %> ID.equal dest) - |> function + Procedure.blocks_succ p src |> Iter.find_pred (ID.equal dest) |> function | Some _ -> (src, dest) | _ -> raise Not_found - let succ p v = Procedure.blocks_succ p v |> Iter.map fst |> Iter.to_list - let pred p v = Procedure.blocks_pred p v |> Iter.map fst |> Iter.to_list + let succ p v = Procedure.blocks_succ p v |> Iter.to_list + let pred p v = Procedure.blocks_pred p v |> Iter.to_list end include Make (BlockGraph) diff --git a/lib/lang/dune b/lib/lang/dune index 9f22039b..45b6a23d 100644 --- a/lib/lang/dune +++ b/lib/lang/dune @@ -14,6 +14,7 @@ block procedure interp + reduction program) (flags -w -27) ; unused var (libraries diff --git a/lib/lang/expr_smt.ml b/lib/lang/expr_smt.ml index 90da5ddc..e03cea3f 100644 --- a/lib/lang/expr_smt.ml +++ b/lib/lang/expr_smt.ml @@ -88,6 +88,35 @@ module SMTLib2 = struct let run (e : 'e t) = e empty + let smt_norm_rewriter e = + let open AbstractExpr in + let open BasilExpr in + let open Bitvec in + let e = AbstractExpr.map fst e in + match e with + | ApplyIntrin { op = `AND; args = [] } -> + replace [%here] @@ BasilExpr.boolconst true + | ApplyIntrin { op = `OR; args = [] } -> + replace [%here] @@ BasilExpr.boolconst false + | ApplyIntrin { op = `Cases; args } -> ( + match List.rev args with + | [ a ] -> replace [%here] (BasilExpr.fix a) + | h :: tl -> + replace [%here] + (List.fold_left + (fun acc b -> + match b with + | BinaryExpr { op = `IfThen; arg1; arg2 } -> + BasilExpr.ifthenelse arg1 arg2 acc + | o -> + (* all other functions are total*) + fix o) + (BasilExpr.fix h) tl) + | _ -> Keep) + | _ -> Keep + + let norm_expr e = BasilExpr.rewrite_typed_two smt_norm_rewriter e + let extract s = let* b = get s in return @@ to_sexp b @@ -174,6 +203,7 @@ module SMTLib2 = struct | `BoolNOT -> atom "not" | `NEQ -> failwith "undef" | `AND -> atom "and" + | `IMPLIES -> atom "=>" | `OR -> atom "or" | #Ops.AllOps.unary as o -> atom @@ Ops.AllOps.to_string o | #Ops.AllOps.const as o -> atom @@ Ops.AllOps.to_string o @@ -250,6 +280,16 @@ module SMTLib2 = struct let* l = l in let* r = r in return @@ list [ of_op o; l; r ] + | ApplyIntrin { op = `Cases; args } -> + let* args = sequence args in + let cond, thn, els = + match args with + | [ condition; `List [ `Atom "case"; arg ]; els ] -> + (condition, arg, els) + | _ -> failwith "unsupp cases" + in + return @@ Bincaml_util.Smt.Expr.ite cond thn els + (* TODO: bool2bv1 *) | ApplyIntrin { op = o; args } -> let* args = sequence args in return (list (of_op o :: args)) @@ -259,8 +299,13 @@ module SMTLib2 = struct let* func = func in return @@ list (func :: args) - let of_bexpr e = fst @@ (BasilExpr.cata smt_alg e) empty - let bind_of_bexpr e b = BasilExpr.cata smt_alg e b + let of_bexpr e = + let e = norm_expr e in + fst @@ (BasilExpr.cata smt_alg e) empty + + let bind_of_bexpr e b = + let e = norm_expr e in + BasilExpr.cata smt_alg e b let trans_decl (decl : Program.declaration) = let* x = return () in @@ -304,7 +349,7 @@ module SMTLib2 = struct | Variable v -> failwith "mutable" let assert_bexpr e = - let* s = BasilExpr.cata smt_alg e in + let* s = bind_of_bexpr e in add_assert s let push = add_command (list [ atom "push" ]) diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 68566673..161635f7 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -274,7 +274,7 @@ end include PG -let add_goto p ~(from : ID.t) ~(targets : ID.t list) = +let add_goto ~(from : ID.t) ~(targets : ID.t list) p = let open Vert in p |> map_graph (fun g -> @@ -338,6 +338,17 @@ let get_entry_block p = Some (List.hd id)) with Not_found -> None +let get_returning_blocks p = + let open Edge in + let open G in + graph p |> Option.to_list + |> List.flat_map (fun g -> + G.pred g Return + |> List.filter_map (function + | Vert.Begin id -> Some id + | End id -> Some id + | _ -> None)) + (** Get the block for an id @raise Not_found when the block does not exist. *) @@ -513,23 +524,19 @@ let blocks_succ p i = |> Iter.flat_map (fun graph -> Iter.from_iter (fun f -> G.iter_succ f graph (End i)) |> Iter.flat_map (function - | Vert.Begin i -> - Iter.singleton - (i, get_block p i |> Option.get_exn_or "bad cfg sturcture") + | Vert.Begin i -> Iter.singleton i | Return -> Iter.empty | Exit -> Iter.empty - | v -> failwith @@ "bad graph structure " ^ Vert.show v)) + | v -> Iter.empty)) let blocks_pred p i = Option.to_iter (graph p) |> Iter.flat_map (fun graph -> Iter.from_iter (fun f -> G.iter_pred f graph (Begin i)) |> Iter.flat_map (function - | Vert.End i -> - Iter.singleton - (i, get_block p i |> Option.get_exn_or "bad cfg sturcture") + | Vert.End i -> Iter.singleton i | Entry -> Iter.empty - | v -> failwith @@ "bad graph structure " ^ Vert.show v)) + | v -> Iter.empty)) let iter_blocks_topo_fwd p = Iter.from_iter (fun f -> fold_blocks_topo_fwd (fun acc a b -> f (a, b)) () p) diff --git a/lib/lang/reduction.ml b/lib/lang/reduction.ml new file mode 100644 index 00000000..e69de29b diff --git a/lib/passes.ml b/lib/passes.ml index dcfd7201..eef71557 100644 --- a/lib/passes.ml +++ b/lib/passes.ml @@ -133,7 +133,7 @@ module PassManager = struct let sssa = { name = "simple-ssa"; - apply = Proc Transforms.Ssa.ssa; + apply = Proc (Transforms.Ssa.ssa %> snd); doc = "Naive SSA transform assuming all variable uses are dominated by \ definitions from parameters"; @@ -153,6 +153,13 @@ module PassManager = struct doc = "Remove blocks unreachable from entry"; } + let verify_smt = + { + name = "verify-procs-smt"; + apply = Prog Transforms.Verif_smt.check; + doc = "Simple smt verification"; + } + let full_ssa = { name = "ssa"; @@ -189,7 +196,7 @@ module PassManager = struct apply = Prog Transforms.Memory_specification.transform; doc = "Specifies programs for memory safety"; } - + let intra_function_summaries = { name = "intra-function-summaries"; @@ -230,6 +237,7 @@ module PassManager = struct read_uninit true; sssa; full_ssa; + verify_smt; type_check; split_memory_encoding; memory_specification; @@ -275,9 +283,9 @@ module PassManager = struct doc = "Replaces captured global variables with explicit parameters"; }; { - name = "gamma-vars"; - apply = Prog Transforms.Gamma_vars.transform; - doc = "Replace gamma expressions with gamma variables"; + name = "gamma-vars"; + apply = Prog Transforms.Gamma_vars.transform; + doc = "Replace gamma expressions with gamma variables"; }; ] diff --git a/lib/transforms/dune b/lib/transforms/dune index b4629843..70d796a1 100644 --- a/lib/transforms/dune +++ b/lib/transforms/dune @@ -14,7 +14,8 @@ memory_specification function_summaries boogie_prepass - gamma_vars) + gamma_vars + verif_smt) (libraries bincaml.analysis patricia-tree diff --git a/lib/transforms/ssa.ml b/lib/transforms/ssa.ml index 4900da25..ba29060d 100644 --- a/lib/transforms/ssa.ml +++ b/lib/transforms/ssa.ml @@ -433,7 +433,11 @@ let set_params ?(skip_observable = true) ?(skip_maps = true) (p : Program.t) = in { p with procs; globals } -let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) = +let ssa ?blocks ?(skip_observable = true) ?(skip_maps = true) + (in_proc : Program.proc) = + let blocks = + Option.get_or ~default:(Procedure.iter_blocks_topo_fwd in_proc) + in let in_proc = intro_ssi_assigns in_proc in let lives = Livevars.run in_proc in let rename r v : Var.t = @@ -537,10 +541,10 @@ let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) = | [] -> Hashtbl.add phis block_id VarMap.empty; (VarMap.empty, []) - | [ (id, _) ] -> (Hashtbl.find st id, []) + | [ id ] -> (Hashtbl.find st id, []) | inc -> let joined_phis = - List.map (fun (id, _) -> (id, get_st_pred id)) inc + List.map (fun id -> (id, get_st_pred id)) inc |> List.fold_left (fun phim (block, rn) -> let rn = @@ -578,7 +582,7 @@ let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) = let renames = Hashtbl.find st block_id in if IDSet.mem block_id !delayed_phis then Procedure.blocks_succ proc block_id - |> Iter.filter (fun (bid, _) -> + |> Iter.filter (fun bid -> let pred = Procedure.G.pred (Option.get_exn_or "unreachable" @@ Procedure.graph proc) @@ -586,7 +590,7 @@ let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) = in List.length pred > 1) |> Iter.fold - (fun proc (succ_bid, _) -> + (fun proc succ_bid -> let eblock = Procedure.get_block proc succ_bid |> Option.get_exn_or "block not exist" @@ -627,9 +631,7 @@ let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) = in let proc = IDSet.fold fixup_delayed !delayed_phis proc in let check_bl (block_id, (block : Program.bloc)) = - let pred = - Procedure.blocks_pred proc block_id |> Iter.map (fun (i, _) -> i) - in + let pred = Procedure.blocks_pred proc block_id |> Iter.map (fun i -> i) in let npred = Iter.length pred in block.phis |> List.map (fun (p : Var.t Block.phi) -> @@ -643,7 +645,7 @@ let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) = in assert (Procedure.iter_blocks_topo_fwd proc |> Iter.for_all check_bl); check_ssa ~skip_observable ~skip_maps proc; - proc + (st, proc) let ssa_prog ?(skip_observable = true) ?(skip_maps = true) (p : Program.t) = - { p with procs = IDMap.map (ssa ~skip_observable ~skip_maps) p.procs } + { p with procs = IDMap.map (ssa ~skip_observable ~skip_maps %> snd) p.procs } diff --git a/lib/transforms/verif_smt.ml b/lib/transforms/verif_smt.ml new file mode 100644 index 00000000..0c59b60b --- /dev/null +++ b/lib/transforms/verif_smt.ml @@ -0,0 +1,331 @@ +(** verify acyclic code *) + +open Bincaml_util.Common +open Lang +open Expr +module MinCut = Graph.Mincut.Make (Procedure.G) +module VertMap = Map.Make (Procedure.Vert) + +let replace_src_in_succs v ~new_src p = + let outgoing = + Procedure.graph p |> Option.to_list + |> List.flat_map (fun g -> Procedure.G.succ_e g v) + in + let new_outgoing = + outgoing |> List.map (function _, l, d -> (new_src, l, d)) + in + p + |> Procedure.map_graph (fun g -> + outgoing |> List.fold_left Procedure.G.remove_edge_e g) + |> Procedure.map_graph (fun g -> + new_outgoing |> List.fold_left Procedure.G.add_edge_e g) + +let replace_dest_in_preds v ~new_dest p = + let incoming = + Procedure.graph p |> Option.to_list + |> List.flat_map (fun g -> Procedure.G.pred_e g v) + in + let new_incoming = + incoming |> List.map (function p, l, _ -> (p, l, new_dest)) + in + p + |> Procedure.map_graph (fun g -> + incoming |> List.fold_left Procedure.G.remove_edge_e g) + |> Procedure.map_graph (fun g -> + new_incoming |> List.fold_left Procedure.G.add_edge_e g) + +let print_vert (v : Procedure.Vert.t) = + match v with + | Begin id -> "bg" ^ String.replace ~sub:"%" ~by:"block" (ID.to_string id) + | End id -> "ed" ^ String.replace ~sub:"%" ~by:"block" (ID.to_string id) + | Entry -> "ORIGentryblock" + | Exit -> "ORIGexitblock" + | Return -> "ORIGretbl" + +module E = struct + type t = { entry : ID.t list; return : ID.t list } +end + +module M = Monad (E) + +let cuts (p : Program.proc) = + let g = Procedure.graph p |> Option.get_exn_or "no graph" in + let cuts = MinCut.min_cutset g Entry in + print_endline @@ (ID.to_string @@ Procedure.id p) ^ " cuts"; + cuts |> List.iter (print_vert %> print_endline); + let pc_width = Z.of_int (List.length cuts) |> Z.numbits %> ( + ) 1 in + let pc_var = + Procedure.fresh_var p ~name:"cut_pc" (Types.Bitvector pc_width) + in + let p = + p |> Procedure.map_formal_in_params (StringMap.add (Var.name pc_var) pc_var) + in + + let pcs = + Procedure.Vert.Entry :: Exit :: Return :: cuts + |> List.to_iter + |> Iter.mapi (fun i v -> (v, Bitvec.of_int i ~size:pc_width)) + |> VertMap.of_iter + in + + let spec = Procedure.specification p in + let pc_guard i = + BasilExpr.binexp ~op:`EQ (BasilExpr.rvar pc_var) + (BasilExpr.bvconst @@ VertMap.find i pcs) + in + let spec = + { + spec with + requires = pc_guard Entry :: spec.requires; + ensures = pc_guard Return :: spec.ensures; + } + in + let p = Procedure.set_specification p spec in + let p, new_entry = Procedure.fresh_block ~stmts:[] ~name:"cut_entry" p () in + let p, new_return = Procedure.fresh_block ~stmts:[] ~name:"cut_return" p () in + let p = + cuts + |> List.fold_left + (fun p v -> + let p, b_begin = + Procedure.fresh_block + ~name:(print_vert v ^ "guard") + ~stmts:[ Instr_Assume { body = pc_guard v; branch = false } ] + p () + in + let p, b_return = + Procedure.fresh_block + ~name:(print_vert v ^ "set_pc") + ~stmts: + [ + Instr_Assign + [ (pc_var, Expr.BasilExpr.bvconst @@ VertMap.find v pcs) ]; + ] + ~successors:[ new_return ] p () + in + let p = + p + |> replace_src_in_succs v ~new_src:(Procedure.Vert.End b_begin) + |> replace_dest_in_preds v + ~new_dest:(Procedure.Vert.Begin new_return) + |> Procedure.add_goto ~from:new_entry ~targets:[ b_begin ] + |> Procedure.add_goto ~from:b_return ~targets:[ new_return ] + in + p) + p + in + let p = replace_src_in_succs Entry ~new_src:(End new_entry) p in + let p = replace_dest_in_preds Return ~new_dest:(Begin new_return) p in + let p = + Procedure.map_graph + (fun g -> Procedure.G.add_edge g Entry (Begin new_entry)) + p + |> Procedure.map_graph (fun g -> + Procedure.G.add_edge g (End new_return) Return) + in + p + +type ftype = { + reach_end : BasilExpr.t list; + assigns : (Var.t * BasilExpr.t) list; + reach_failure : BasilExpr.t list; +} + +let extract p = + let entry_block = + Procedure.graph p |> Option.get_exn_or "" |> fun g -> + Procedure.G.succ g Entry + |> List.filter_map (function + | Procedure.Vert.Begin id -> Some id + | End id -> Some id + | _ -> None) + in + let block_done id = + Var.create ("block_done_" ^ ID.to_string id) Types.Boolean + in + let stmt e (s : Program.stmt) = + match s with + | Instr_Assert { body } -> + let rfail = + BasilExpr.binexp ~op:`IMPLIES + (BasilExpr.applyintrin ~op:`AND e.reach_end) + (BasilExpr.unexp ~op:`BoolNOT body) + in + { + e with + reach_end = body :: e.reach_end; + reach_failure = rfail :: e.reach_failure; + } + | Instr_Assume { body } -> { e with reach_end = body :: e.reach_end } + | Instr_Assign assigns -> { e with assigns = assigns @ e.assigns } + | _ -> failwith "unsupported" + in + let phi e (s : 'a Block.phi) = + match s with + | { lhs; rhs } -> + let rhs = + rhs + |> List.map (fun (bid, v) -> + BasilExpr.binexp ~op:`IfThen + (BasilExpr.rvar (block_done bid)) + (BasilExpr.rvar v)) + in + let cases = BasilExpr.applyintrin ~op:`Cases rhs in + { e with assigns = (lhs, cases) :: e.assigns } + in + let phi = List.fold_left phi in + let g = Procedure.graph p |> Option.get_exn_or "" in + let assigns = + Procedure.fold_blocks_topo_fwd + (fun acc id b -> + print_endline (ID.to_string id); + let r_fail, prog = acc in + let e = + if List.exists (ID.equal id) entry_block then BasilExpr.boolconst true + else + let preds = + Procedure.blocks_pred p id + |> Iter.map (block_done %> BasilExpr.rvar) + |> Iter.to_list + in + BasilExpr.applyintrin ~op:`OR preds + in + + let st = { assigns = []; reach_end = [ e ]; reach_failure = [] } in + let st = Block.fold_forwards ~phi ~f:stmt st b in + let st = + { + st with + assigns = + (block_done id, BasilExpr.applyintrin ~op:`AND st.reach_end) + :: st.assigns; + } + in + (st.reach_failure, Iter.cons (e, st.assigns) prog)) + ([], Iter.empty) p + in + let exits = Procedure.get_returning_blocks p in + let terminates = + BasilExpr.applyintrin ~op:`OR + @@ List.map (block_done %> BasilExpr.rvar) exits + in + let fails = BasilExpr.applyintrin ~op:`OR (fst assigns) in + let spec = Procedure.specification p in + let requires = BasilExpr.applyintrin ~op:`AND spec.requires in + let ensures = BasilExpr.applyintrin ~op:`AND spec.ensures in + let cond = + BasilExpr.binexp ~op:`IMPLIES requires + (BasilExpr.applyintrin ~op:`AND + [ BasilExpr.unexp ~op:`BoolNOT fails; terminates; ensures ]) + in + (cond, snd assigns) + +let to_smt (cond, assigns) = + let open Expr_smt.SMTLib2 in + let open Bincaml_util.Smt in + let query = + assigns + |> Iter.fold + (fun (acc : builder) (cond, assigns) -> + let assigns = + List.map + (fun (l, r) -> BasilExpr.binexp ~op:`EQ (BasilExpr.rvar l) r) + assigns + in + let b = + Expr_smt.SMTLib2.assert_bexpr + (BasilExpr.binexp ~op:`IMPLIES cond + @@ BasilExpr.applyintrin ~op:`AND assigns) + in + snd @@ b acc) + Expr_smt.SMTLib2.empty + in + let _, b = (assert_bexpr (BasilExpr.unexp ~op:`BoolNOT cond)) query in + let sexp = to_sexp ~set_logic:true b in + sexp + +let succ e = + match e with + | `Atom "success" -> () + | e -> failwith ("not success: " ^ Sexp.to_string e) + +let check s i e = + let open Bincaml_util.Smt in + Solver.push s; + e |> Iter.iter (fun x -> Bincaml_util.Smt.Solver.add_command s x); + let e = Solver.check s in + let m = + match e with + | Unsat -> "ok" + | Sat -> "failed: " ^ (Solver.get_model s |> Sexp.to_string) + | Unknown -> "unkown" + in + Printf.printf "%s : %s\n" (ID.to_string i) m; + Solver.pop s; + e + +(* Need to perform check at prog level to resolve inteprocedural effects; calls + + +(1) lift to lambda parameter form +(2) interpreocedural effects +(2) per procedure: + + 2.1 identify cut points & introduce PC assignments and guards + 2.2 perform ssa and stash result + 2.3 compute liveness result + 2.4 add the live variables at each entry cut in params and exit cut to out params. + + 2.5 chop cut points and redirect through entry/exit, add loop ssa-rewritten invariant + assertion + + (can we do the loop invariant vc insertion earlier - at 2.1?) + while (c) invariant q {x}; ~> + assert q; while (c) (assume q ; x; assert q) assert q; + + at entry assume: + (1) pc = entry => precondition + (2) pc = header => header inv[ssa(header)] + + at exit assert: + (1) pc = header => header inv[ssa(header)] + (2) pc = backedge => header inv[ssa(backedge)] + (3) pc = return => postcondition + + 2.6 perform reachability reduction of now DAG procedure + + + + + +*) +let check (p : Program.t) = + let op = p in + let p = Ssa.set_params ~skip_observable:false ~skip_maps:false p in + let p = { p with procs = IDMap.map cuts p.procs } in + (* + let fixed = + IDMap.map Cleanup_cfg.remove_blocks_unreachable_from_entry fixed + in + *) + + let p = Ssa.ssa_prog ~skip_observable:false ~skip_maps:false p in + IDMap.iter + (fun k p -> + CCIO.with_out + (ID.to_string k ^ "dotgraph.dot") + (fun v -> + Viscfg.Dot.output_graph v + (Procedure.graph p |> Option.get_exn_or "procedure has no graph"))) + p.procs; + + let smts = IDMap.map extract p.procs in + let s = + Bincaml_util.Smt.Solver.create + { + Bincaml_util.Smt.Config.cvc5 with + log = Bincaml_util.Smt.Config.printf_log; + } + in + let _ = IDMap.map to_smt smts |> IDMap.mapi (check s) in + op diff --git a/lib/util/smt.ml b/lib/util/smt.ml index f8327433..230c1c76 100644 --- a/lib/util/smt.ml +++ b/lib/util/smt.ml @@ -496,12 +496,12 @@ module Expr = struct | `Atom x -> (x, []) | `List xs -> ( match xs with - | y :: ys -> begin - match y with + | y :: ys -> + begin match y with | `Atom x -> (x, ys) | `List [ _; `Atom x; _ ] -> (x, ys) (*cvc5: (as con ty)*) | _ -> bad () - end + end | _ -> bad ()) (** {1 Commands} @@ -743,11 +743,11 @@ end = struct match todo with | x :: xs -> if StringSet.mem x !processed then arrange xs - else begin - if StringSet.mem x !processing then + else + begin if StringSet.mem x !processing then raise (UnexpectedSolverResponse ans) (* recursive *) - else begin - match StringMap.find_opt x deps with + else + begin match StringMap.find_opt x deps with | None -> arrange xs | Some (ds, e) -> processing := StringSet.add x !processing; @@ -756,8 +756,8 @@ end = struct processed := StringSet.add x !processed; decls := drop_as_array e :: !decls; arrange xs + end end - end | [] -> () in arrange (List.map (fun (x, _, _) -> x) defs);