Top-Down Synthesizer

class qsynthesis.algorithms.synthesizer_td.TopDownSynthesizer(ltms: InputOutputOracle | List[InputOutputOracle], only_first_match: bool = False, learning_new_exprs: bool = False)

Bases: SynthesizerBase

Synthesize with a Top-Down only AST search based on Triton AST. The complexity in worst case of the search is then O(n) with n the number of nodes in the AST to synthesize.

Constructor that takes one or multiple oracles as input.

Parameters:

• ltms – Single oracle or a list

• only_first_match – boolean that stop interating over tables as soon as the lookup is successfull for one

• learning_new_exprs – boolean that enables improving the current table if if a synthesized entry appears to be bigger than the one submitted

eval_ast(ioast: TritonAst, input: qsynthesis.types.Input) → qsynthesis.types.Output

Run evaluation of the TritonAst ioast on the given Input (valuation for all vars). The result is an Output (integer)

Parameters:

• ioast (TritonAst) – TritonAst to evaluate

• input (qsynthesis.types.Input) – Input on which to evaluate the AST. All variables of ioast must be defined in input

Returns:

Output which is the result of evaluation (made by Triton)

Return type:

qsynthesis.types.Output

run_direct_synthesis(ltm: InputOutputOracle, cur_ast: TritonAst) → TritonAst | None

Evaluate cur_ast on inputs provided by ltm the oracle which provide an output vector then used to perform the lookup in the database. If an entry is found it is returned.

Parameters:

• ltm – InputOutputOracle object in which to perform the query

• cur_ast – TritonAst object to synthesize

Returns:

optional TritonAst if the an entry was found

synthesize(ioast: TritonAst, check_sem: bool = False) → Tuple[TritonAst, bool]

Perform the Top-Down search on the ioast to try synthesizing it. The algorithm first tries to synthesize the root node. If not successful descend recursively in all children of the AST to try substituting sub-ASTs.

Parameters:

• ioast – TritonAst object to synthesize

• check_sem – boolean one whether to check the semantic equivalence of expression before substituting them. That ensure soundness of the synthesis

Returns:

tuple with new TritonAst and whether some replacement took place or not

Warning

Activating the check_sem parameter implies a strong overhead on the synthesis as SMT queries are being performed for any candidates

try_synthesis_lookup(cur_ast: TritonAst, check_sem: bool = False) → TritonAst | None

Performs a direct synthesis lookup. And returns an optional TritonAst if it the I/O evaluation has been found in one of the tables. Unlike SynthesizerBase.synthesize() which can go down the AST to try simplifying sub-AST here only the root node is attempted to be synthesized.

Parameters:

• cur_ast – TritonAst to synthesize

• check_sem – boolean on whether to check the semantic equivalence of expression before performing substituting.

Returns:

optional TritonAst if the the AST has been synthesized

Placeholder-based Synthesizer

class qsynthesis.algorithms.synthesizer_plhld.PlaceHolderSynthesizer(ltms: InputOutputOracle | List[InputOutputOracle], only_first_match: bool = False, learning_new_exprs: bool = False)

Bases: TopDownBottomUpSynthesizer

Synthesizer inherited from TopDownBottomUpSynthesizer which thus form the search in that manner. The specificity of this synthesizer is to temporarily replacing synthesized expressions with a placeholder variable that will ‘abstract the behavior of the synthesized AST’. The intended effect is to recursively synthesized previously synthesized sub-AST (with these placeholders). At the end of the search all placeholder variables are substituted by their associated synthesized expression.

Constructor that takes lookup tables as input.

Parameters:

• ltms – Single lookup table of a list of them

• only_first_match – boolean that stop interating over tables as soon as the lookup is successfull for one

• learning_new_exprs – boolean that enables improving the current table if if a synthesized entry appears to be bigger than the one submitted

eval_ast(ioast: TritonAst, input: qsynthesis.types.Input) → qsynthesis.types.Output

Run evaluation of the TritonAst ioast on the given Input (valuation for all vars). The result is an Output (integer)

Parameters:

• ioast (TritonAst) – TritonAst to evaluate

• input (qsynthesis.types.Input) – Input on which to evaluate the AST. All variables of ioast must be defined in input

Returns:

Output which is the result of evaluation (made by Triton)

Return type:

qsynthesis.types.Output

replace_all(ast: TritonAst, replacement: Dict[TritonAst, TritonAst], recursive: bool = False) → None

Performs the final replacement of Placeholder variable with their synthesized expression equivalence in ast provided in parameter.

Parameters:

• ast – TritonAst object in which to perform all substitutions

• replacement – dictionnary of placeholder variable as TritonAst to synthesized expression (TritonAst)

• recursive – whether to also perform the substitution in synthesized expressions given in the dictionnary

Returns:

None as the ast object is modified in place

Warning

All the expressions to replace should be present only once because TritonAst objects are not deepcopied. Thus duplicating it at various location of the AST would be various dangerous for attributes coherence when calling update

run_direct_synthesis(ltm: InputOutputOracle, cur_ast: TritonAst) → TritonAst | None

Evaluate cur_ast on inputs provided by ltm the oracle which provide an output vector then used to perform the lookup in the database. If an entry is found it is returned.

Parameters:

• ltm – InputOutputOracle object in which to perform the query

• cur_ast – TritonAst object to synthesize

Returns:

optional TritonAst if the an entry was found

synthesize(ioast: TritonAst, check_sem: bool = False) → Tuple[TritonAst, bool]

Performs the placeholder based top-down and then bottom-up search for synthesizing the given TritonAst.

Parameters:

• ioast – TritonAst object to synthesize

• check_sem – boolean one whether to check the semantic equivalence of expression before substituting them. That ensure soundness of the synthesis

Returns:

tuple with new TritonAst and whether some replacement took place or not

Warning

Activating the check_sem parameter implies a strong overhead on the synthesis as SMT queries are being performed for any candidates

try_synthesis_lookup(cur_ast: TritonAst, check_sem: bool = False) → TritonAst | None

Performs a direct synthesis lookup. And returns an optional TritonAst if it the I/O evaluation has been found in one of the tables. Unlike SynthesizerBase.synthesize() which can go down the AST to try simplifying sub-AST here only the root node is attempted to be synthesized.

Parameters:

• cur_ast – TritonAst to synthesize

• check_sem – boolean on whether to check the semantic equivalence of expression before performing substituting.

Returns:

optional TritonAst if the the AST has been synthesized