docs/notebooks/PICS/FuzzingWithConstraints-synopsis-1.svg

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
 "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 9.0.0 (20230911.1827)
 -->
<!-- Pages: 1 -->
<svg width="226pt" height="88pt"
 viewBox="0.00 0.00 226.25 88.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 84)">
<g id="a_graph0"><a xlink:title="ISLaSolver class hierarchy">
<polygon fill="white" stroke="none" points="-4,4 -4,-84 222.25,-84 222.25,4 -4,4"/>
</a>
</g>
<!-- ISLaSolver -->
<g id="node1" class="node">
<title>ISLaSolver</title>
<g id="a_node1"><a xlink:href="isla.solver.ipynb" xlink:title="class ISLaSolver:&#10;The solver class for ISLa formulas/constraints. Its top&#45;level methods are&#10;&#10;:meth:`~isla.solver.ISLaSolver.solve`&#10;Use to generate solutions for an ISLa constraint.&#10;&#10;:meth:`~isla.solver.ISLaSolver.check`&#10;Use to check if an ISLa constraint is satisfied for a given input.&#10;&#10;:meth:`~isla.solver.ISLaSolver.parse`&#10;Use to parse and validate an input.&#10;&#10;:meth:`~isla.solver.ISLaSolver.repair`&#10;Use to repair an input such that it satisfies a constraint.&#10;&#10;:meth:`~isla.solver.ISLaSolver.mutate`&#10;Use to mutate an input such that the result satisfies a constraint.">
<polygon fill="none" stroke="black" points="0,-0.5 0,-79.5 81.25,-79.5 81.25,-0.5 0,-0.5"/>
<text text-anchor="start" x="8" y="-63.2" font-family="Patua One, Helvetica, sans-serif" font-weight="bold" font-size="14.00" fill="#b03a2e">ISLaSolver</text>
<polyline fill="none" stroke="black" points="0,-53.5 81.25,-53.5"/>
<g id="a_node1_0"><a xlink:href="#" xlink:title="ISLaSolver">
<g id="a_node1_1"><a xlink:href="isla.solver.ipynb" xlink:title="__init__(self, grammar: Union[Dict[str, List[str]], str], formula: Union[isla.language.Formula, str, NoneType] = None, structural_predicates: Set[isla.language.StructuralPredicate] = frozenset({StructuralPredicate(name=&#39;different_position&#39;, arity=2, eval_fun=&lt;function is_different_position&gt;), StructuralPredicate(name=&#39;consecutive&#39;, arity=2, eval_fun=&lt;function consecutive&gt;), StructuralPredicate(name=&#39;level&#39;, arity=4, eval_fun=&lt;function level_check&gt;), StructuralPredicate(name=&#39;before&#39;, arity=2, eval_fun=&lt;function is_before&gt;), StructuralPredicate(name=&#39;inside&#39;, arity=2, eval_fun=&lt;function in_tree&gt;), StructuralPredicate(name=&#39;nth&#39;, arity=3, eval_fun=&lt;function is_nth&gt;), StructuralPredicate(name=&#39;after&#39;, arity=2, eval_fun=&lt;function is_after&gt;), StructuralPredicate(name=&#39;same_position&#39;, arity=2, eval_fun=&lt;function is_same_position&gt;), StructuralPredicate(name=&#39;direct_child&#39;, arity=2, eval_fun=&lt;function is_direct_child&gt;)}), semantic_predicates: Set[isla.language.SemanticPredicate] = frozenset({SemanticPredicate(count, 3)}), 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, cost_computer: Optional[ForwardRef(&#39;CostComputer&#39;)] = None, timeout_seconds: Optional[int] = None, global_fuzzer: bool = False, predicates_unique_in_int_arg: Tuple[isla.language.SemanticPredicate, ...] = (SemanticPredicate(count, 3),), fuzzer_factory: Callable[[Dict[str, List[str]]], isla.fuzzer.GrammarFuzzer] = &lt;function SolverDefaults.&lt;lambda&gt;&gt;, tree_insertion_methods: Optional[int] = None, activate_unsat_support: bool = False, grammar_unwinding_threshold: int = 4, initial_tree: isla.helpers.Maybe[isla.derivation_tree.DerivationTree] = Maybe(a=None), enable_optimized_z3_queries: bool = True, start_symbol: Optional[str] = None):&#10;The constructor of :class:`~isla.solver.ISLaSolver` accepts a large number of&#10;parameters. However, all but the first one, :code:`grammar`, are *optional.*&#10;&#10;The simplest way to construct an ISLa solver is by only providing it with a&#10;grammar only; it then works like a grammar fuzzer.&#10;&#10;&gt;&gt;&gt; import random&#10;&gt;&gt;&gt; random.seed(1)&#10;&#10;&gt;&gt;&gt; import string&#10;&gt;&gt;&gt; LANG_GRAMMAR = {&#10;... &#160;&#160;&#160;&#160;&quot;&lt;start&gt;&quot;:&#10;... &#160;&#160;&#160;&#160;&#160;&#160;&#160;&#160;[&quot;&lt;stmt&gt;&quot;],&#10;... &#160;&#160;&#160;&#160;&quot;&lt;stmt&gt;&quot;:&#10;... &#160;&#160;&#160;&#160;&#160;&#160;&#160;&#160;[&quot;&lt;assgn&gt; ; &lt;stmt&gt;&quot;, &quot;&lt;assgn&gt;&quot;],&#10;... &#160;&#160;&#160;&#160;&quot;&lt;assgn&gt;&quot;:&#10;... &#160;&#160;&#160;&#160;&#160;&#160;&#160;&#160;[&quot;&lt;var&gt; := &lt;rhs&gt;&quot;],&#10;... &#160;&#160;&#160;&#160;&quot;&lt;rhs&gt;&quot;:&#10;... &#160;&#160;&#160;&#160;&#160;&#160;&#160;&#160;[&quot;&lt;var&gt;&quot;, &quot;&lt;digit&gt;&quot;],&#10;... &#160;&#160;&#160;&#160;&quot;&lt;var&gt;&quot;: list(string.ascii_lowercase),&#10;... &#160;&#160;&#160;&#160;&quot;&lt;digit&gt;&quot;: list(string.digits)&#10;... }&#10;&gt;&gt;&gt;&#10;&gt;&gt;&gt; from isla.solver import ISLaSolver&#10;&gt;&gt;&gt; solver = ISLaSolver(LANG_GRAMMAR)&#10;&gt;&gt;&gt;&#10;&gt;&gt;&gt; str(solver.solve())&#10;&#39;d := 9&#39;&#10;&gt;&gt;&gt; str(solver.solve())&#10;&#39;v := n ; s := r&#39;&#10;&#10;:param grammar: The underlying grammar; either, as a &quot;Fuzzing Book&quot; dictionary&#10;or in BNF syntax.&#10;:param formula: The formula to solve; either a string or a readily parsed&#10;formula. If no formula is given, a default `true` constraint is assumed, and&#10;the solver falls back to a grammar fuzzer. The number of produced solutions&#10;will then be bound by `max_number_free_instantiations`.&#10;:param structural_predicates: Structural predicates to use when parsing a&#10;formula.&#10;:param semantic_predicates: Semantic predicates to use when parsing a formula.&#10;:param max_number_free_instantiations: Number of times that nonterminals that&#10;are not bound by any formula should be expanded by a coverage&#45;based fuzzer.&#10;:param max_number_smt_instantiations: Number of solutions of SMT formulas that&#10;should be produced.&#10;:param max_number_tree_insertion_results: The maximum number of results when&#10;solving existential quantifiers by tree insertion.&#10;:param enforce_unique_trees_in_queue: If true, states with the same tree as an&#10;already existing tree in the queue are discarded, irrespectively of the&#10;constraint.&#10;:param debug: If true, debug information about the evolution of states is&#10;collected, notably in the field state_tree. The root of the tree is in the&#10;field state_tree_root. The field costs stores the computed cost values for&#10;all new nodes.&#10;:param cost_computer: The `CostComputer` class for computing the cost relevant&#10;to placing states in ISLa&#39;s queue.&#10;:param timeout_seconds: Number of seconds after which the solver will terminate.&#10;:param global_fuzzer: If set to True, only one coverage&#45;guided grammar fuzzer&#10;object is used to finish off unconstrained open derivation trees throughout&#10;the whole generation time. This may be beneficial for some targets; e.g., we&#10;experienced that CSV works significantly faster. However, the achieved k&#45;path&#10;coverage can be lower with that setting.&#10;:param predicates_unique_in_int_arg: This is needed in certain cases for&#10;instantiating universal integer quantifiers. The supplied predicates should&#10;have exactly one integer argument, and hold for exactly one integer value&#10;once all other parameters are fixed.&#10;:param fuzzer_factory: Constructor of the fuzzer to use for instantiating&#10;&quot;free&quot; nonterminals.&#10;:param tree_insertion_methods: Combination of methods to use for existential&#10;quantifier elimination by tree insertion. Full selection: `DIRECT_EMBEDDING &amp;&#10;SELF_EMBEDDING &amp; CONTEXT_ADDITION`.&#10;:param activate_unsat_support: Set to True if you assume that a formula might&#10;be unsatisfiable. This triggers additional tests for unsatisfiability that&#10;reduce input generation performance, but might ensure termination (with a&#10;negative solver result) for unsatisfiable problems for which the solver could&#10;otherwise diverge.&#10;:param grammar_unwinding_threshold: When querying the SMT solver, ISLa passes a&#10;regular expression for the syntax of the involved nonterminals. If this&#10;syntax is not regular, we unwind the respective part in the reference grammar&#10;up to a depth of `grammar_unwinding_threshold`. If this is too shallow, it can&#10;happen that an equation etc. cannot be solved; if it is too deep, it can&#10;negatively impact performance (and quite tremendously so).&#10;:param initial_tree: An initial input tree for the queue, if the solver shall&#10;not start from the tree `(&lt;start&gt;, None)`.&#10;:param enable_optimized_z3_queries: Enables preprocessing of Z3 queries (mainly&#10;numeric problems concerning things like length). This can improve performance&#10;significantly; however, it might happen that certain problems cannot be solved&#10;anymore. In that case, this option can/should be deactivated.&#10;:param start_symbol: This is an alternative to `initial_tree` for starting with&#10;a start symbol different form `&lt;start&gt;`. If `start_symbol` is provided, a tree&#10;consisting of a single root node with the value of `start_symbol` is chosen as&#10;initial tree.">
<text text-anchor="start" x="10.62" y="-41" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-weight="bold" font-size="10.00">__init__()</text>
</a>
</g>
<g id="a_node1_2"><a xlink:href="isla.solver.ipynb" xlink:title="check(self, inp: isla.derivation_tree.DerivationTree | str) &#45;&gt; bool:&#10;Evaluates whether the given derivation tree satisfies the constraint passed to&#10;the solver. Raises an `UnknownResultError` if this could not be evaluated&#10;(e.g., because of a solver timeout or a semantic predicate that cannot be&#10;evaluated).&#10;&#10;:param inp: The input to evaluate, either readily parsed or as a string.&#10;:return: A truth value.">
<text text-anchor="start" x="10.62" y="-29.75" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-weight="bold" font-size="10.00">check()</text>
</a>
</g>
<g id="a_node1_3"><a xlink:href="isla.solver.ipynb" xlink:title="parse(self, inp: str, nonterminal: str = &#39;&lt;start&gt;&#39;, skip_check: bool = False, silent: bool = False) &#45;&gt; isla.derivation_tree.DerivationTree:&#10;Parses the given input `inp`. Raises a `SyntaxError` if the input does not&#10;satisfy the grammar, a `SemanticError` if it does not satisfy the constraint&#10;(this is only checked if `nonterminal` is &quot;&lt;start&gt;&quot;), and returns the parsed&#10;`DerivationTree` otherwise.&#10;&#10;:param inp: The input to parse.&#10;:param nonterminal: The nonterminal to start parsing with, if a string&#10;corresponding to a sub&#45;grammar shall be parsed. We don&#39;t check semantic&#10;correctness in that case.&#10;:param skip_check: If True, the semantic check is left out.&#10;:param silent: If True, no error is sent to the log stream in case of a&#10;failed parse.&#10;:return: A parsed `DerivationTree`.">
<text text-anchor="start" x="10.62" y="-18.5" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-weight="bold" font-size="10.00">parse()</text>
</a>
</g>
<g id="a_node1_4"><a xlink:href="isla.solver.ipynb" xlink:title="solve(self) &#45;&gt; isla.derivation_tree.DerivationTree:&#10;Attempts to compute a solution to the given ISLa formula. Returns that solution,&#10;if any. This function can be called repeatedly to obtain more solutions until&#10;one of two exception types is raised: A :class:`StopIteration` indicates that&#10;no more solution can be found; a :class:`TimeoutError` is raised if a timeout&#10;occurred. After that, an exception will be raised every time.&#10;&#10;The timeout can be controlled by the :code:`timeout_seconds`&#10;:meth:`constructor &lt;isla.solver.ISLaSolver.__init__&gt;` parameter.&#10;&#10;:return: A solution for the ISLa formula passed to the&#10;:class:`isla.solver.ISLaSolver`.">
<text text-anchor="start" x="10.62" y="-7.25" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-weight="bold" font-size="10.00">solve()</text>
</a>
</g>
</a>
</g>
</a>
</g>
</g>
<!-- Legend -->
<g id="node2" class="node">
<title>Legend</title>
<text text-anchor="start" x="99" y="-56" font-family="Patua One, Helvetica, sans-serif" font-weight="bold" font-size="10.00" fill="#b03a2e">Legend</text>
<text text-anchor="start" x="99" y="-46" font-family="Patua One, Helvetica, sans-serif" font-size="10.00">• </text>
<text text-anchor="start" x="105" y="-46" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-weight="bold" font-size="8.00">public_method()</text>
<text text-anchor="start" x="99" y="-36" font-family="Patua One, Helvetica, sans-serif" font-size="10.00">• </text>
<text text-anchor="start" x="105" y="-36" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-size="8.00">private_method()</text>
<text text-anchor="start" x="99" y="-26" font-family="Patua One, Helvetica, sans-serif" font-size="10.00">• </text>
<text text-anchor="start" x="105" y="-26" font-family="'Fira Mono', 'Source Code Pro', 'Courier', monospace" font-style="italic" font-size="8.00">overloaded_method()</text>
<text text-anchor="start" x="99" y="-16.95" font-family="Helvetica,sans-Serif" font-size="9.00">Hover over names to see doc</text>
</g>
</g>
</svg>