QSynthesis documentation
QSynthesis is a Python API to perform Greybox synthesis of bitvector expressions. The base synthesis algorithm is based on both a blackbox I/O based approach comparing solely input-to-output pairs to perform the synthesis, but also a whitebox AST search to synthesize sub-expressions (if the root expression cannot be synthesized all at once). Also, instead of deriving possible candidates on each expressions to synthesize, QSynthesis relies on pre-computated expressions stored in a database. The database keeps the mapping of an expression and its associated output vector representing its behavior on a set of inputs. Given a bitvector expression to synthesize, finding a candidate can thus be performed in near O(1) as the lookup is the lookup cost in database. With the structure used (Google Level-DB) the cost is thus Log(N) with N the number of entries in the database.
Getting started
Plugin Usage
Python API
- TritonAst
TritonAstTritonAst.compare_behavior()TritonAst.depthTritonAst.duplicate()TritonAst.dyn_depth()TritonAst.dyn_node_count()TritonAst.eval_oracle()TritonAst.from_z3()TritonAst.get_children()TritonAst.has_children()TritonAst.hashTritonAst.is_constant()TritonAst.is_constant_expr()TritonAst.is_leaf()TritonAst.is_root()TritonAst.is_semantically_equal()TritonAst.is_variable()TritonAst.make_ast()TritonAst.make_graph()TritonAst.mappingTritonAst.mk_constant()TritonAst.mk_variable()TritonAst.node_countTritonAst.normalized_str_to_ast()TritonAst.parentsTritonAst.pp_strTritonAst.ptr_idTritonAst.random_sampling()TritonAst.reassemble()TritonAst.replace_self()TritonAst.set_child()TritonAst.sub_mapTritonAst.symbolTritonAst.symvar_type()TritonAst.symvarsTritonAst.to_normalized_str()TritonAst.to_z3()TritonAst.typeTritonAst.update()TritonAst.update_all()TritonAst.update_parents()TritonAst.var_numTritonAst.variable_idTritonAst.visit_expr()TritonAst.visit_replacement()
- Top-Down Synthesizer
- Placeholder-based Synthesizer
- Grammar
- Oracles
InputOutputOracleInputOutputOracle.add_entries()InputOutputOracle.add_entry()InputOutputOracle.bitsizeInputOutputOracle.create()InputOutputOracle.generate()InputOutputOracle.hash()InputOutputOracle.input_numberInputOutputOracle.is_expr_compatible()InputOutputOracle.is_writableInputOutputOracle.load()InputOutputOracle.lookup()InputOutputOracle.lookup_hash()InputOutputOracle.nameInputOutputOracle.operator_numberInputOutputOracle.sizeInputOutputOracle.var_number
- Symbolic Execution utilities
- Types