**Problem Detail:**

Is there a way to generate a set of inputs, for a given output of a function? This may be a common thing in lisp/haskell world, but I'm not aware of it. Is this what mini-kanren does?

I understand that there may not be a general solution to this problem, since the halting problem may apply here. Say the function implementation is constrained to remove unlimited recursion. Type inference engines obviously do something similar to figure out the types of variables, I would like to generate actual values.

I'm thinking of a couple of scenarios where this might be useful:

`func blowup(x): 1/x `

I would like some sort of static checker to figure out that this function will cause problems if x=0.

`func launch(x): ...launch missle x miles... func isSafe(y): if x > 10 then true else false func main(): x=.1; if isSafe(x): launch(x) `

In this case, I would like to not only infer values of launch, but I would like to take isSafe as a constraint and tell me at compile time (since all information is available) that x of .1 not a good value.

Btw, I'm not looking for a library to do this. What I would love is either the name of this concept (beyond the generic 'static checking') and reference material which describes this idea (easily read papers, books, etc.). I should also mention that I'm aware of tools such as quickcheck. I'm not looking for a probabilistic way of inferring values. I would like a deterministic way of inferring values as early as possible, even if that means that my solution limits the types of expressions I can express.

###### Asked By : Shahbaz

#### Answered By : D.W.

In the worst case, this is impossible. However, there are techniques for inversion that can work on some programs. Of course, you shouldn't expect them to work on all programs given that the problem is hard.

Here are a few standard approaches:

**Theorem proving.**Use the VCGen part of a theorem prover to generate a precondition formula, where if the formula is true, that implies that the function produces the desired output (or divides by zero, etc.). Then, use an automated solver to try to find a satisfying assignment to that formula.**Symbolic execution.**Execute the function symbolically, and build up a symbolic expression that represents the output of the function, in terms of a bunch of variables (unknowns) that represent the inputs to the function. Then build a formula by setting that expression equal to the desired output, feed that formula to a SMT solver and ask the solver to find a satisfying assignment for the formula.**Concolic execution.**Pick concrete values for the inputs to the function. Execute the function on those inputs and record what path it took. On the side, build up a symbolic expression that represents the output of the function, if it follows the same path. Build up a "path constraint", which is a formula that is the conjunction of all of the branch conditions followed: the path constraint is a formula over symbolic variables representing the inputs, where inputs that make the path constraint true will cause the function to execute the same path that was previously recorded. Then, write down a formula that represents the statement "the function takes that path, and its output is equal to the desired value", and feed this to a SMT solver or SAT solver and ask it to find a satisfying assignment. See concolic testing.

These approaches have different tradeoffs and perform differently, but as you can see, they are similar conceptually. Here are some significant differences:

Theorem proving and symbolic execution can have problems with loops. For instance, theorem provers usually require you to supply a loop invariant for every loop. Concolic execution circumvents this by not trying to reason about all possible paths; only a single one.

Theorem proving and symbolic execution can have problems with state space explosion, as the number of possible paths through the function can be exponentially (or even infinitely) large. Concolic execution circumvents this by not trying to reason about all possible paths; only a single one.

Theorem proving can use more expressive logics, such as fist-order logic. Symbolic execution and concolic execution often use propositional logic or a SMT extension.

You can find lots of reference material on these approaches. For instance, today they're taught in a number of advanced (e.g., graduate) program analysis courses, and there are many publications in the research literature on these topics.

###### Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/46953

**3.2K people like this**

## 0 comments:

## Post a Comment

Let us know your responses and feedback