5
$\begingroup$

Let's say I have a program P, in form of a binary code for x86 architecture.

I want to find a Boolean formula F (in form of CNF, or something like that), such that F(input,output) = true iff P(input) = output So to answer a question "what output does the program produce on given input" I will only need to run a SAT/SMT solver for X on formula F(input,X) == true. I understand that this problem is undecidable in general case, but I only care for some practical cases.

What keywords should I google to find more about this topic?

Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ I'd look into The Cook-Levin Theorem. It seems pretty similar to what you want. $\endgroup$
    – testuser
    Commented Nov 6, 2018 at 16:23
  • $\begingroup$ @testuser: you should post your comment as a proper answer so that it can be accepted. Maybe add one or two sentences about how the proof goes. $\endgroup$
    – Andrej Bauer
    Commented Nov 6, 2018 at 17:53
  • $\begingroup$ @testuser As I understand Cook-Levin Theorem says about translation of problems into SAT, but I want to translate a program, not a problem. I want something like program synthesis in reverse: when from a program you get a specification of which constrains between input and output are implied by the program. $\endgroup$
    – Arqwer
    Commented Nov 6, 2018 at 18:23
  • 1
    $\begingroup$ @Arqwer You can translate the problem $P(x,y) = $"program $A$ on input $x$ outputs $y$". Isn't translating $P$ the same thing as translating the program $A$, for your purposes? $\endgroup$
    – chi
    Commented Nov 6, 2018 at 19:25

2 Answers 2

Reset to default
2
$\begingroup$

I understand that this problem is undecidable in general case, but I only care for some practical cases.

This is impossible if the program contains complicated loops

  • infinite loops
  • loops that depend on the value of the input, e.g. for(int i = 0; i < input; ++i)
  • ...

For program where loops can be unfolded, you can construct such a formula using either Bounded Model Checking or Symbolic Execution.

You are asking about x86 machine code, which is very difficult for program analysis, as disassembly alone can be very imprecise.

For C programs, you can use CBMC to translate a program into either a SAT or SMT formula. All the details of the translation can be found on this technical report. http://shelf2.library.cmu.edu/Tech/52490804.pdf

Improve this answer
$\endgroup$
7
$\begingroup$

Disclaimer: I'm not sure how useful any of this is for getting this done practically since you have a program, not a Turing Machine.

The Cook-Levin Theorem essentially states that you can translate the execution of a Turing Machine into a boolean formula that is polynomial in the length of the TM's execution such that the formula is satisfiable iff the TM accepts the input.

In your case 'accepts' means 'returns true'. One could model this in a TM by transitioning to an accepting state instead of returning true.

The linked Wiki article gives a good exposition of the proof but the gist if it is that you have variables that describe the input to the machine, the sequence of states the machine takes during an execution, the position of the head during an execution, and a bunch of conjunctions that force satisfying assignment of the variables to describe a successful execution of the TM on the input.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.