nonterminal_positions = [ i for i, x in enumerate(matching_expansion) if x == next_nonterminal ] for nonterminal_position in nonterminal_positions: next_children = [ - DerivationTree(nonterm, []) - if idx != nonterminal_position - else DerivationTree(nonterm, None) + ( + DerivationTree(nonterm, []) + if idx != nonterminal_position + else DerivationTree(nonterm, None) + ) for idx, nonterm in enumerate(matching_expansion) ] new_candidate = candidate.replace_path( leaf_path, DerivationTree(leaf_node, next_children)

assert isinstance(start_node, NonterminalNode) prefixes: List[Tuple[Set[Node], List[Node]]] = [ ( - set() - if start_node == dest_node and graph.reachable(start_node, start_node) - else {start_node}, + ( + set() + if start_node == dest_node and graph.reachable(start_node, start_node) + else {start_node} + ), [start_node], ) ] result: OrderedSet[Tuple[str, ...]] = OrderedSet([])

return 1 + max(child.depth() for child in self.children) def new_ids(self) -> "DerivationTree": return DerivationTree( self.value, - None - if self.children is None - else [child.new_ids() for child in self.children], + ( + None + if self.children is None + else [child.new_ids() for child in self.children] + ), ) def __len__(self): if self.__len is None: self.__len = len(self.paths())

} if not nonterminal_expansions: return [] - possible_expansions: List[ - Dict[Path, List[DerivationTree]] - ] = dict_of_lists_to_list_of_dicts(nonterminal_expansions) + possible_expansions: List[Dict[Path, List[DerivationTree]]] = ( + dict_of_lists_to_list_of_dicts(nonterminal_expansions) + ) assert ( len(possible_expansions) > 1 or len(possible_expansions) == 1 and possible_expansions[0]

assert isinstance(reference_tree, DerivationTree) subtrees_trie = reference_tree.trie() if subtrees_trie is None else subtrees_trie graph = gg.GrammarGraph.from_grammar(grammar) if graph is None else graph formula = instantiate_top_level_constant( - parse_isla(formula, grammar, structural_predicates, semantic_predicates) - if isinstance(formula, str) - else formula, + ( + parse_isla(formula, grammar, structural_predicates, semantic_predicates) + if isinstance(formula, str) + else formula + ), reference_tree, ) # NOTE: Deactivated, might be too strict for evaluation (though maybe # necessary for solving). See comment in well_formed.

) -> Maybe[ThreeValuedTruth]: if not isinstance(formula, StructuralPredicateFormula): return Nothing arg_insts = [ - arg - if isinstance(arg, str) - else next( - path for path, subtree in reference_tree.paths() if subtree.id == arg.id - ) - if isinstance(arg, DerivationTree) - else assignments[arg][0] + ( + arg + if isinstance(arg, str) + else ( + next( + path + for path, subtree in reference_tree.paths() + if subtree.id == arg.id + ) + if isinstance(arg, DerivationTree) + else assignments[arg][0] + ) + ) for arg in formula.args ] return Some( ThreeValuedTruth.from_bool( formula.predicate.evaluate(reference_tree, *arg_insts)

) -> Maybe[ThreeValuedTruth]: if not isinstance(formula, SemanticPredicateFormula): return Nothing arg_insts = [ - arg - if isinstance(arg, DerivationTree) or arg not in assignments - else assignments[arg][1] + ( + arg + if isinstance(arg, DerivationTree) or arg not in assignments + else assignments[arg][1] + ) for arg in formula.args ] eval_res = formula.predicate.evaluate(graph, *arg_insts) if eval_res.true():

common_nonterminal_prefixes: List[Path] = [tuple()] for idx in range(min(len(path_1), len(path_2))): if path_1[idx] != path_2[idx]: break - prefix = path_1[:idx + 1] # should consider a prefix up to and including the current index + prefix = path_1[ + : idx + 1 + ] # should consider a prefix up to and including the current index if context_tree.get_subtree(prefix).value == nonterminal: common_nonterminal_prefixes.append(prefix) for prefix in common_nonterminal_prefixes: nonterminal_occs_1, nonterminal_occs_2 = [

print("ERROR: timeout value must be an integer.", file=sys.stderr) print_help() exit(1) self.jobs_and_generators = { - f"{jobname_prefix} {job}": generator - if isinstance(generator, dict) - else generator(self.timeout) + f"{jobname_prefix} {job}": ( + generator if isinstance(generator, dict) else generator(self.timeout) + ) for job, generator in zip(jobnames, generators) if job in chosen_jobs } try:

store_inputs(jobname, self.timeout, inputs, self.db_file) continue with pmp.Pool(processes=pmp.cpu_count()) as pool: pool.starmap( - lambda jobname, generator: generate_inputs( - generator, self.timeout, jobname - ) - if self.dry_run - else store_inputs( - jobname, - self.timeout, - generate_inputs(generator, self.timeout, jobname), - self.db_file, + lambda jobname, generator: ( + generate_inputs(generator, self.timeout, jobname) + if self.dry_run + else store_inputs( + jobname, + self.timeout, + generate_inputs(generator, self.timeout, jobname), + self.db_file, + ) ), list(self.jobs_and_generators.items()), ) def evaluate_validity(self) -> None:

] = [ ( [jobname], [self.validator], [self.db_file], - sids[jobname] - if self.num_sessions < 0 - else sids[jobname][len(sids[jobname]) - self.num_sessions :], + ( + sids[jobname] + if self.num_sessions < 0 + else sids[jobname][len(sids[jobname]) - self.num_sessions :] + ), ) for jobname in self.jobs_and_generators ] args: List[

( [jobname], [self.graph], [k], [self.db_file], - sids[jobname] - if self.num_sessions < 0 - else sids[jobname][len(sids[jobname]) - self.num_sessions :], + ( + sids[jobname] + if self.num_sessions < 0 + else sids[jobname][len(sids[jobname]) - self.num_sessions :] + ), ) for jobname in self.jobs_and_generators for k in self.kvalues ]

def strtime() -> str: return datetime.now().strftime("%H:%M:%S") def generate_inputs( - generator: Generator[isla.derivation_tree.DerivationTree, None, None] - | ISLaSolver - | Grammar, + generator: ( + Generator[isla.derivation_tree.DerivationTree, None, None] + | ISLaSolver + | Grammar + ), timeout_seconds: int = 60, jobname: Optional[str] = None, ) -> Dict[float, isla.derivation_tree.DerivationTree]: start_time = time.time() result: Dict[float, isla.derivation_tree.DerivationTree] = {}

return result def make_input_generator( - generator: Generator[isla.derivation_tree.DerivationTree, None, None] - | ISLaSolver - | Grammar + generator: ( + Generator[isla.derivation_tree.DerivationTree, None, None] + | ISLaSolver + | Grammar + ) ) -> Generator[isla.derivation_tree.DerivationTree, None, None]: if isinstance(generator, ISLaSolver): def gen(): while True:

) -> Union[bool, str]: contents = "int main() {\n" contents += "\n" + str(tree).replace("\n", " \t") contents += "\n" + "}" - with tempfile.NamedTemporaryFile(suffix=".c") as tmp, tempfile.NamedTemporaryFile( - suffix=".o" - ) as outfile: + with ( + tempfile.NamedTemporaryFile(suffix=".c") as tmp, + tempfile.NamedTemporaryFile(suffix=".o") as outfile, + ): tmp.write(contents.encode()) tmp.flush() cmd = ["clang", tmp.name, "-o", outfile.name] process = subprocess.Popen(cmd, stderr=PIPE) (stdout, stderr) = process.communicate()

return merge_intervals( *map( lambda option_or_union: numeric_intervals_from_regex( z3.Concat(option_or_union, *children[1:]) ), - first_child.children() - if first_child.decl().kind() == z3.Z3_OP_RE_UNION - else [z3.Re("+"), z3.Re("-")], + ( + first_child.children() + if first_child.decl().kind() == z3.Z3_OP_RE_UNION + else [z3.Re("+"), z3.Re("-")] + ), ) ) elif first_child in [z3.Re("+"), z3.Option(z3.Re("+"))]: return numeric_intervals_from_regex( children[1] if len(children) == 2 else z3.Concat(*children[1:])

@DataClass(frozen=True) class SolverDefaults: formula: Optional[language.Formula | str] = None - structural_predicates: frozenset[ - language.StructuralPredicate - ] = STANDARD_STRUCTURAL_PREDICATES - semantic_predicates: frozenset[ - language.SemanticPredicate - ] = STANDARD_SEMANTIC_PREDICATES + structural_predicates: frozenset[language.StructuralPredicate] = ( + STANDARD_STRUCTURAL_PREDICATES + ) + semantic_predicates: frozenset[language.SemanticPredicate] = ( + STANDARD_SEMANTIC_PREDICATES + ) max_number_free_instantiations: int = 10 max_number_smt_instantiations: int = 10 max_number_tree_insertion_results: int = 5 enforce_unique_trees_in_queue: bool = False debug: bool = False

timeout_seconds: Optional[int] = None global_fuzzer: bool = False predicates_unique_in_int_arg: Tuple[language.SemanticPredicate, ...] = ( COUNT_PREDICATE, ) - fuzzer_factory: Callable[ - [Grammar], GrammarFuzzer - ] = lambda grammar: GrammarCoverageFuzzer(grammar) + fuzzer_factory: Callable[[Grammar], GrammarFuzzer] = ( + lambda grammar: GrammarCoverageFuzzer(grammar) + ) tree_insertion_methods: Optional[int] = None activate_unsat_support: bool = False grammar_unwinding_threshold: int = 4 initial_tree: Maybe[DerivationTree] = Nothing enable_optimized_z3_queries: bool = True

self.solutions: List[DerivationTree] = [] # Debugging stuff self.debug = debug - self.state_tree: Dict[ - SolutionState, List[SolutionState] - ] = {} # is only filled if self.debug + self.state_tree: Dict[SolutionState, List[SolutionState]] = ( + {} + ) # is only filled if self.debug self.state_tree_root = None self.current_state = None self.costs: Dict[SolutionState, float] = {} if self.debug:

for abstracted_tree in generate_abstracted_trees(inp, participating_paths): match ( safe(lambda: self.check(abstracted_tree))() .bind(lambda _: Nothing) .lash( - lambda exc: Some(abstracted_tree) - if isinstance(exc, UnknownResultError) - else Nothing + lambda exc: ( + Some(abstracted_tree) + if isinstance(exc, UnknownResultError) + else Nothing + ) ) .bind(do_complete) ): case Some(completed): return Some(completed)

# We also try to falsify (negated) semantic predicate formulas, if present, # if there exist any remaining disjuncts. semantic_predicate_formulas: List[ Tuple[language.SemanticPredicateFormula, bool] ] = [ - (pred_formula, False) - if isinstance(pred_formula, language.SemanticPredicateFormula) - else (cast(language.NegatedFormula, pred_formula).args[0], True) + ( + (pred_formula, False) + if isinstance(pred_formula, language.SemanticPredicateFormula) + else (cast(language.NegatedFormula, pred_formula).args[0], True) + ) for pred_formula in language.FilterVisitor( lambda f: ( constant in f.free_variables() and ( isinstance(f, language.SemanticPredicateFormula)

) existential_formula = cast( language.ExistsFormula, conjuncts[existential_formula_idx] ) - matches: List[ - Dict[language.Variable, Tuple[Path, DerivationTree]] - ] = matches_for_quantified_formula(existential_formula, self.grammar) + matches: List[Dict[language.Variable, Tuple[Path, DerivationTree]]] = ( + matches_for_quantified_formula(existential_formula, self.grammar) + ) for match in matches: inst_formula = existential_formula.inner_formula.substitute_expressions( {variable: match_tree for variable, (_, match_tree) in match.items()} )

tap( lambda intervals: formulas.append( z3_or( [ z3.And( - repl_var >= z3.IntVal(interval[0]) - if interval[0] > -sys.maxsize - else z3.BoolVal(True), - repl_var <= z3.IntVal(interval[1]) - if interval[1] < sys.maxsize - else z3.BoolVal(True), + ( + repl_var >= z3.IntVal(interval[0]) + if interval[0] > -sys.maxsize + else z3.BoolVal(True) + ), + ( + repl_var <= z3.IntVal(interval[1]) + if interval[1] < sys.maxsize + else z3.BoolVal(True) + ), ) for interval in intervals ] ) )

z3.Concat(z3.Range("1", "9"), z3.Star(z3.Range("0", "9"))), ) elif constant in tree_substitutions: # We have a more concrete shape of the desired instantiation available regexes = [ - self.extract_regular_expression(t) - if is_nonterminal(t) - else z3.Re(t) + ( + self.extract_regular_expression(t) + if is_nonterminal(t) + else z3.Re(t) + ) for t in split_str_with_nonterminals( str(tree_substitutions[constant]) ) ] assert regexes

and not self.graph.reachable(elem, nonterminal) for elem in canonical_expansions[0] ) ): result_elements: List[z3.ReRef] = [ - z3.Re(elem) - if not is_nonterminal(elem) - else self.extract_regular_expression(elem) + ( + z3.Re(elem) + if not is_nonterminal(elem) + else self.extract_regular_expression(elem) + ) for elem in canonical_expansions[0] ] return self.regex_cache.setdefault(nonterminal, z3.Concat(*result_elements)) regex_conv = RegexConverter(

( expanded_tree, curr_len + sum( [ - len(child.value) - if child.children == () - else (1 if child.value not in nullable else 0) + ( + len(child.value) + if child.children == () + else (1 if child.value not in nullable else 0) + ) for child in new_children ] ) - int(leaf.value not in nullable), open_leaves[:idx]

def subtree_solutions( solution: Dict[language.Constant | DerivationTree, DerivationTree] ) -> Dict[language.Variable | DerivationTree, DerivationTree]: - solution_with_subtrees: Dict[ - language.Variable | DerivationTree, DerivationTree - ] = {} + solution_with_subtrees: Dict[language.Variable | DerivationTree, DerivationTree] = ( + {} + ) for orig, subst in solution.items(): if isinstance(orig, language.Variable): solution_with_subtrees[orig] = subst continue

in_nonterminal: str, immutable_grammar: ImmutableGrammar, ) -> Maybe[Tuple[DerivationTree, Dict[BoundVariable, Path]]]: flattened_bind_expr_str = "".join( map( - lambda elem: f"{{{elem.n_type} {elem.name}}}" - if type(elem) is BoundVariable - else str(elem), + lambda elem: ( + f"{{{elem.n_type} {elem.name}}}" + if type(elem) is BoundVariable + else str(elem) + ), bound_elements, ) ) maybe_tree = parse_match_expression(

# TODO: Check if `()` is always the right choice for the children match_expr_tree = match_expr_tree.replace_path( path, DerivationTree( child.value, - () + (), # None if is_nonterminal(child.value) else () ), ) skip_paths_below.add(path)

return f'BindExpression({", ".join(map(repr, self.bound_elements))})' def __str__(self): return "".join( map( - lambda e: f"{str(e)}" - if isinstance(e, str) - else ("[" + "".join(map(str, e)) + "]") - if isinstance(e, list) - else ( - f"{{{e.n_type} {str(e)}}}" - if not isinstance(e, DummyVariable) - else str(e) + lambda e: ( + f"{str(e)}" + if isinstance(e, str) + else ( + ("[" + "".join(map(str, e)) + "]") + if isinstance(e, list) + else ( + f"{{{e.n_type} {str(e)}}}" + if not isinstance(e, DummyVariable) + else str(e) + ) + ) ), self.bound_elements, ) )

and self.args == other.args ) def __str__(self): arg_strings = [ - f'"{arg}"' - if isinstance(arg, str) - else ( - arg.to_string(show_open_leaves=True, show_ids=True) - if isinstance(arg, DerivationTree) - else str(arg) + ( + f'"{arg}"' + if isinstance(arg, str) + else ( + arg.to_string(show_open_leaves=True, show_ids=True) + if isinstance(arg, DerivationTree) + else str(arg) + ) ) for arg in self.args ] return f"{self.predicate}({', '.join(arg_strings)})"

def substitute_variables(self, subst_map: Dict[Variable, Variable]): assert not self.already_matched return ForallFormula( - self.bound_variable - if self.bound_variable not in subst_map - else subst_map[self.bound_variable], - self.in_variable - if self.in_variable not in subst_map - else subst_map[self.in_variable], + ( + self.bound_variable + if self.bound_variable not in subst_map + else subst_map[self.bound_variable] + ), + ( + self.in_variable + if self.in_variable not in subst_map + else subst_map[self.in_variable] + ), self.inner_formula.substitute_variables(subst_map), - None - if not self.bind_expression - else self.bind_expression.substitute_variables(subst_map), + ( + None + if not self.bind_expression + else self.bind_expression.substitute_variables(subst_map) + ), self.already_matched, id=self.id, ) def substitute_expressions(

): super().__init__(bound_variable, in_variable, inner_formula, bind_expression) def substitute_variables(self, subst_map: Dict[Variable, Variable]): return ExistsFormula( - self.bound_variable - if self.bound_variable not in subst_map - else subst_map[self.bound_variable], - self.in_variable - if self.in_variable not in subst_map - else subst_map[self.in_variable], + ( + self.bound_variable + if self.bound_variable not in subst_map + else subst_map[self.bound_variable] + ), + ( + self.in_variable + if self.in_variable not in subst_map + else subst_map[self.in_variable] + ), self.inner_formula.substitute_variables(subst_map), - None - if not self.bind_expression - else self.bind_expression.substitute_variables(subst_map), + ( + None + if not self.bind_expression + else self.bind_expression.substitute_variables(subst_map) + ), ) def substitute_expressions( self, subst_map: Dict[Union[Variable, DerivationTree], DerivationTree] ) -> Formula:

# For all other formulas, we add a single quantifier around them as a whole if other_formulas: result_elements += [ univ_close_over_var_push_in( - type(formula)(*other_formulas) - if len(other_formulas) > 1 - else other_formulas[0], + ( + type(formula)(*other_formulas) + if len(other_formulas) > 1 + else other_formulas[0] + ), var, in_var, mexpr, qfd_vars, )

""" return tuple( [ tuple( [ - (elem, 0) - if "[" not in elem - else (elem.split("[")[0], int(elem.split("[")[1][:-1]) - 1) + ( + (elem, 0) + if "[" not in elem + else (elem.split("[")[0], int(elem.split("[")[1][:-1]) - 1) + ) for elem in seg.split(".") ] ) for seg in xpath_expr.split("..") ]

partial_tree.replace_path( path_to_expand, DerivationTree( partial_tree.get_subtree(path_to_expand).value, [ - DerivationTree(elem) - if is_nonterminal(elem) - else DerivationTree(elem, []) + ( + DerivationTree(elem) + if is_nonterminal(elem) + else DerivationTree(elem, []) + ) for elem in expansion ], ), ) ] = paths[:-1] + [

def enterExists(self, ctx: IslaLanguageParser.ExistsContext): self.enterQfdFormula(ctx) def exitQfdFormula( self, - ctx: IslaLanguageParser.ForallContext - | IslaLanguageParser.ExistsContext - | IslaLanguageParser.ForallMexprContext - | IslaLanguageParser.ExistsMexprContext, + ctx: ( + IslaLanguageParser.ForallContext + | IslaLanguageParser.ExistsContext + | IslaLanguageParser.ForallMexprContext + | IslaLanguageParser.ExistsMexprContext + ), mexpr=False, ): is_forall = str(ctx.children[0]) == "forall" if mexpr:

def exitSexprPrefix(self, ctx: IslaLanguageParser.SexprPrefixContext): if not ctx.sexpr(): self.smt_expressions[ctx] = parse_tree_text(ctx.op) else: - self.smt_expressions[ - ctx - ] = f'({parse_tree_text(ctx.op)} {" ".join([self.smt_expressions[child] for child in ctx.sexpr()])})' + self.smt_expressions[ctx] = ( + f'({parse_tree_text(ctx.op)} {" ".join([self.smt_expressions[child] for child in ctx.sexpr()])})' + ) def exitSexprInfixReStr(self, ctx: IslaLanguageParser.SexprInfixReStrContext): - self.smt_expressions[ - ctx - ] = f"({parse_tree_text(ctx.op)} {self.smt_expressions[ctx.sexpr(0)]} {self.smt_expressions[ctx.sexpr(1)]})" + self.smt_expressions[ctx] = ( + f"({parse_tree_text(ctx.op)} {self.smt_expressions[ctx.sexpr(0)]} {self.smt_expressions[ctx.sexpr(1)]})" + ) def exitSexprInfixPlusMinus( self, ctx: IslaLanguageParser.SexprInfixPlusMinusContext ): - self.smt_expressions[ - ctx - ] = f"({parse_tree_text(ctx.op)} {self.smt_expressions[ctx.sexpr(0)]} {self.smt_expressions[ctx.sexpr(1)]})" + self.smt_expressions[ctx] = ( + f"({parse_tree_text(ctx.op)} {self.smt_expressions[ctx.sexpr(0)]} {self.smt_expressions[ctx.sexpr(1)]})" + ) def exitSexprInfixMulDiv(self, ctx: IslaLanguageParser.SexprInfixMulDivContext): - self.smt_expressions[ - ctx - ] = f"({parse_tree_text(ctx.op)} {self.smt_expressions[ctx.sexpr(0)]} {self.smt_expressions[ctx.sexpr(1)]})" + self.smt_expressions[ctx] = ( + f"({parse_tree_text(ctx.op)} {self.smt_expressions[ctx.sexpr(0)]} {self.smt_expressions[ctx.sexpr(1)]})" + ) def exitSexprInfixEq(self, ctx: IslaLanguageParser.SexprInfixEqContext): - self.smt_expressions[ - ctx - ] = f"({parse_tree_text(ctx.op)} {self.smt_expressions[ctx.sexpr(0)]} {self.smt_expressions[ctx.sexpr(1)]})" + self.smt_expressions[ctx] = ( + f"({parse_tree_text(ctx.op)} {self.smt_expressions[ctx.sexpr(0)]} {self.smt_expressions[ctx.sexpr(1)]})" + ) # def exitSepxrParen(self, ctx: IslaLanguageParser.SepxrParenContext): # self.smt_expressions[ctx] = self.smt_expressions[ctx.sexpr()] def exitSepxrApp(self, ctx: IslaLanguageParser.SepxrAppContext):

return "".join(escape_char(char) for char in elem) return "\n".join( f"{symbol} ::= " + " | ".join( - '""' - if not expansion - else " ".join( - (elem if is_nonterminal(elem) else f'"{escape_string(elem)}"') - for elem in expansion + ( + '""' + if not expansion + else " ".join( + (elem if is_nonterminal(elem) else f'"{escape_string(elem)}"') + for elem in expansion + ) ) for expansion in expansions ) for symbol, expansions in canonical(grammar).items() )

parser = EarleyParser(specialized_grammar) for _ in range(3): inp = "".join( [ - str(fuzzer.expand_tree(DerivationTree(v.n_type))) - if is_nonterminal(v.n_type) - else v.n_type + ( + str(fuzzer.expand_tree(DerivationTree(v.n_type))) + if is_nonterminal(v.n_type) + else v.n_type + ) for v in combination ] ) try: next(iter(parser.parse(inp)))

Process completed with exit code 1.