One common method of finding out the needed input to reach a specific execution flow (or a target instruction/function) is done using SMT solvers.
SMT solvers are programs that accept a set of symbols, potentially conflicting conditions and a set of defined operations between them, as well as a desired outcome/target. An SMT solver will attempt to provide a "solution" to the given constraints, in the defined domain space.
As mentioned, this topic is tightly related to fuzzing and symbolic execution, of course. That is also the main context in which SMT solvers (and similar techniques/approaches) are used in the security industry. Couple folks in the industry have also spent a lot of their time on that, namely Rolf Rolles.
There are a few SMT solvers that are commonly used in the security industry community (that I'm aware of):
- Z3 by Microsoft is a widely known one.
- Triton is another.
- angr is a library focused on lifting assembly to IR and solving constraints.
Additionally, there are a
bunch ton of solvers over at the wiki page.