From c31c8ba72f21085656583712d0a79579317a39db Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Tue, 30 Jun 2026 09:42:03 +0100 Subject: [PATCH 1/2] [injector] Unfold rules at the recursive end of the rule To optimize depth calculation, unfolding of recursive rules should only be done at the recursive end of the rule i.e., in a graph with: ``` A -> B -> C -> A ``` Unfolding to k-depth should yield: ``` A_k := B_k B_k := C_k C_k := A_{k - 1} ``` This is acheived using a sort of topological sort on recursive rules to obtain an order to break up loops. --- src/injector/call_graph.ml | 18 ++++++---- src/injector/transform.ml | 70 ++++++++++++++++++++++++-------------- 2 files changed, 55 insertions(+), 33 deletions(-) diff --git a/src/injector/call_graph.ml b/src/injector/call_graph.ml index d4bf7f0..325fd9c 100644 --- a/src/injector/call_graph.ml +++ b/src/injector/call_graph.ml @@ -10,7 +10,9 @@ let get_dependencies (rule : Rule.t) : StringSet.t = | Terminal _ | Range _ -> acc | Star atom | Plus atom | Opt atom -> atom_deps acc atom | Group body -> - List.fold_left (fun acc case -> List.fold_left atom_deps acc case) acc body + List.fold_left + (fun acc case -> List.fold_left atom_deps acc case) + acc body in List.fold_left (fun acc case -> List.fold_left atom_deps acc case) @@ -24,17 +26,19 @@ let build (rules : Rule.t list) : t = let dependencies name cg = StringMap.find_opt name cg |> Option.value ~default:StringSet.empty -let recursive_nonterminals cg = - let nodes = StringMap.bindings cg |> List.map fst in - let rec can_reach start target visited = +let can_reach cg start target = + let rec loop start target visited = if StringSet.mem start visited then false else let deps = dependencies start cg in if StringSet.mem target deps then true else StringSet.exists - (fun next -> can_reach next target (StringSet.add start visited)) + (fun next -> loop next target (StringSet.add start visited)) deps in - List.filter (fun node -> can_reach node node StringSet.empty) nodes - |> StringSet.of_list + loop start target StringSet.empty + +let recursive_nonterminals cg = + let nodes = StringMap.bindings cg |> List.map fst in + List.filter (fun node -> can_reach cg node node) nodes |> StringSet.of_list diff --git a/src/injector/transform.ml b/src/injector/transform.ml index 4ae5bad..407d4b7 100644 --- a/src/injector/transform.ml +++ b/src/injector/transform.ml @@ -5,39 +5,57 @@ let unfold (rules : Rule.t list) (k : int) : Rule.t list = let cg = Call_graph.build rules in let recursive = Call_graph.recursive_nonterminals cg in - let make_name name i = Printf.sprintf "%s_%d" name i in - - let rec is_recursive_atom = function - | Non_terminal id -> StringSet.mem id recursive - | Terminal _ | Range _ -> false - | Star atom | Plus atom -> is_recursive_atom atom - | Group body -> List.exists is_recursive_case body + (* Create an ordering of non-terminals to break cycles exactly once *) + let order = + List.mapi (fun i (r : Rule.t) -> (r.name, i)) rules + |> List.to_seq |> StringMap.of_seq + in + let get_order name = + StringMap.find_opt name order |> Option.value ~default:0 + in - and is_recursive_case case = List.exists is_recursive_atom case in + let make_name name i = Printf.sprintf "%s_%d" name i in - let rec transform_atom i atom = + let rec transform_atom current_name i atom = match atom with - | Terminal _ | Range _ -> atom - | Star atom -> Star (transform_atom i atom) - | Plus atom -> Plus (transform_atom i atom) - | Group body -> Group (List.map (transform_case i) body) + | Terminal _ | Range _ -> Some atom + | Star atom -> + Option.map (fun a -> Star a) (transform_atom current_name i atom) + | Plus atom -> + Option.map (fun a -> Plus a) (transform_atom current_name i atom) + | Opt atom -> + Option.map (fun a -> Opt a) (transform_atom current_name i atom) + | Group body -> + let new_body = List.filter_map (transform_case current_name i) body in + if List.is_empty new_body then None else Some (Group new_body) | Non_terminal id -> - if StringSet.mem id recursive then Non_terminal (make_name id i) - else Non_terminal id - - and transform_case i case = List.map (transform_atom i) case in + if StringSet.mem id recursive then + let next_i = + if + Call_graph.can_reach cg id current_name + && get_order id <= get_order current_name + then i - 1 + else i + in + if next_i < 0 then None else Some (Non_terminal (make_name id next_i)) + else Some (Non_terminal id) + and transform_case current_name i case = + let rec loop acc = function + | [] -> Some (List.rev acc) + | hd :: tl -> ( + match transform_atom current_name i hd with + | None -> None + | Some a -> loop (a :: acc) tl ) + in + loop [] case + in let build_new_rules rule = let rec loop acc i = if i < 0 then acc else let new_name = make_name rule.name i in - let new_body = - if i = 0 then - (* Filter out cases that contain recursive calls *) - List.filter (fun case -> not (is_recursive_case case)) rule.body - else List.map (transform_case (i - 1)) rule.body - in + let new_body = List.filter_map (transform_case rule.name i) rule.body in let new_rule = { name = new_name; body = new_body } in loop (new_rule :: acc) (i - 1) in @@ -49,10 +67,10 @@ let unfold (rules : Rule.t list) (k : int) : Rule.t list = (fun acc rule -> if StringSet.mem rule.name recursive then build_new_rules rule @ acc else - (* Not recursive one might call recursive ones *) - let new_rule = - { name = rule.name; body = List.map (transform_case k) rule.body } + let new_body = + List.filter_map (transform_case rule.name k) rule.body in + let new_rule = { name = rule.name; body = new_body } in new_rule :: acc ) [] rules in From 4cd9108f8443556ce005e093c95ec2f86ebd6a4a Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Tue, 30 Jun 2026 09:48:34 +0100 Subject: [PATCH 2/2] Promote tests --- test/injector/complete/test_basic.t | 20 ++++++++++++++------ test/injector/unit/test_features.ml | 3 ++- test/injector/verify/test_basic.t | 18 +++++++++++++----- 3 files changed, 29 insertions(+), 12 deletions(-) diff --git a/test/injector/complete/test_basic.t b/test/injector/complete/test_basic.t index 7e2699d..2af4267 100644 --- a/test/injector/complete/test_basic.t +++ b/test/injector/complete/test_basic.t @@ -9,10 +9,10 @@ Basic completion: ::= "b" | "d"; Unfolding level: Unfolded grammar (k = 3): - ::= "a" | "c"; - ::= "a" | "c"; - ::= "a" | "c"; - ::= "c"; + ::= "a" | "c"; + ::= "a" | "c"; + ::= "a" | "c"; + ::= "a" | "c"; ::= "b" | "d"; ::= "b" | "d"; ::= "b" | "d"; @@ -22,8 +22,16 @@ Basic completion: SMT Expr: (str.in_re x (regexp.union (regexp.++ - (regexp.union (regexp.++ (str.to_re "c") (str.to_re "b")) + (regexp.union + (regexp.++ + (regexp.union + (regexp.++ + (regexp.union + (regexp.++ + (regexp.union (regexp.++ (str.to_re "d") (str.to_re "a")) + (str.to_re "c")) (str.to_re "b")) (str.to_re "d")) + (str.to_re "a")) (str.to_re "c")) (str.to_re "b")) (str.to_re "d")) (str.to_re "a")) (str.to_re "c"))) Satisfying model: (model - (x str "cba")) + (x str "daba")) diff --git a/test/injector/unit/test_features.ml b/test/injector/unit/test_features.ml index 8e9223e..d487517 100644 --- a/test/injector/unit/test_features.ml +++ b/test/injector/unit/test_features.ml @@ -1,6 +1,7 @@ open Injector -let test_grammar_features = {| +let test_grammar_features = + {| ::= [a-z] [A-Z] [0-9]; ::= "a"* *; ::= "b"+ [0-9]+; diff --git a/test/injector/verify/test_basic.t b/test/injector/verify/test_basic.t index 939c25c..7d0288d 100644 --- a/test/injector/verify/test_basic.t +++ b/test/injector/verify/test_basic.t @@ -9,10 +9,10 @@ Basic verification: ::= "b" | "d"; Unfolding level: Unfolded grammar (k = 3): - ::= "a" | "c"; - ::= "a" | "c"; - ::= "a" | "c"; - ::= "c"; + ::= "a" | "c"; + ::= "a" | "c"; + ::= "a" | "c"; + ::= "a" | "c"; ::= "b" | "d"; ::= "b" | "d"; ::= "b" | "d"; @@ -22,6 +22,14 @@ Basic verification: SMT Expr: (str.in_re "cba" (regexp.union (regexp.++ - (regexp.union (regexp.++ (str.to_re "c") (str.to_re "b")) + (regexp.union + (regexp.++ + (regexp.union + (regexp.++ + (regexp.union + (regexp.++ + (regexp.union (regexp.++ (str.to_re "d") (str.to_re "a")) + (str.to_re "c")) (str.to_re "b")) (str.to_re "d")) + (str.to_re "a")) (str.to_re "c")) (str.to_re "b")) (str.to_re "d")) (str.to_re "a")) (str.to_re "c"))) Candiate 'cba' is a valid sentence of A_2