Function Extraction: Mapping Programs into Mathematica Equations

My talk is called Function Extraction Mapping Programs into Mathematical Equations. So the history of this is that we have been using Mathematica to extract the function of C like programs since 2007. And then after a while I published everything I had to say about this and I was done. But my co author, Richard Linger contacted me back and said that actually that work lends itself to a product that we can use at scale. So then we resumed work on this about two years ago and I am hereby reporting on what we are at. So I will talk about what does it mean to extract the function of the program? How do we do this? By transforming source code into a program function. Of course, the bottleneck of this is how we compute the function of loops. And that has been an obstacle for a long time. And so we will discuss that. Then we will discuss how that falls into the overall goal of computing program functions. Then if you have time, I will talk briefly about some scalable ways to do that. So computing the function of a program is really a decades old dream. People usually refer to this as symbolic execution, as a way to test programs for a wide range of inputs. But in the absence of the ability to capture the function of loops, what people have done in the past is they compute the function of one execution path at a time. But of course all programs have an infinity of execution paths. So this is important to be able to do this for, to be able to draw precise, automatically generated documentation because it supports reuse and also because it exposes malicious functionality. So what makes malicious code dangerous is not that the program is incorrect. It's not that the program fails to do what it's supposed to do. Rather it's because the program is doing something it's not supposed to do. So all the verification you can think of will never catch the fact that the program is doing something in hiding. So we proceed in three steps. First of all, we go from source code, in this case Java, but it could be any other C like language, into an abstract syntax tree using common parsers. Then we transform the abstract syntax tree into a mathematical equation that involves the input and the output of the program, or if you wish, the initial state and the final state. And then from then on, it's up to Mathematica. Whatever Mathematica can do, we can do. So the third step is to go from the mathematical equation to the program function. In effect, what we generate is an equation of the form eq. Of initial state, final state. And then we rely on Mathematica. If it can change that into a functional form which says SP equal F of S. And the focus of our work obviously is the second step. So as an example, I take a very simple program that's the abstract syntax tree for it, and the mathematical equation for it is what you see on the left. And then when we ask Mathematica to generate a function, we get the description on the right. Sorry, I take a slightly more complex program this time, but this time I have loops in it. So there is a branching logic that is a while loop there, a while loop here, a while loop here with a for loop inside it. And my guess is if I. If I ask 100 programmers with 20 years experience minimum to tell me what this program is doing, I would be lucky if one of them could. Alternatively, we can push a button and ask the program, the system to tell us and yeah, so this is the abstract syntax read, doesn't matter. This is the function that the program is computing. And the first comment or the first observation to make is the original code had three branches. So the case where I greater than J, the case where j greater than I else the case where I is equal to J. And you wonder why is it that the function has two branches? The function has only a branch for I less than j and the branch for I equal J. Then I go back to the code and I say what happened with the first branch? And if you look at the first branch, you see that they have a loop here where I is increased by K, then I decrement K, then I decrease I by K, I subtract I from K, meaning that at each iteration I Increase I by 1, and you notice that the loop exits if I is equal to J. So you are increasing I by one every time, waiting for I to be equal to J. But wait a minute. But I enter this loop, I enter this branch only if I is greater than J, meaning whenever I enter this branch, I never terminate. Okay? When you try to compute the function of this program, you will find that the case of I greater than J is not there. It only terminates if I is less than or equal to J. The other thing you find is here it says I equal J, but j greater than equal to zero, meaning if J is not greater than equal to zero, I am not going to terminate. And if you go back, you see why? Because here I am increasing, yeah, here I am increasing T by one and I am waiting for T to be equal to I. But you notice that T has been set to I minus J, and I am entering this branch only if I is equal to j, meaning when I enter, T is equal to 0 and I am increasing T by 1 each time, waiting for it to be equal to I. The only way this will work is if I is greater than zero. And because I is equal to J, Mathematica said j greater than equal to zero, which is the same thing. Okay, so this here is telling me under what condition this program will terminate. And it is telling me each time what happens when the program terminates. So in this case it's computing some combination of Fibonacci functions. In the other case it's computing some arithmetic expression. So what I wanted to show is this here is the mathematical equation that is generated for that small program. So then the nesting in the equation is a reflection of the nesting in the source code. And the parts that I highlight, I will come back to them in a minute. These are the parts that stem from trying to evaluate the loops. Okay, so how do we compute loop functions? By introducing the concept of an invariant relation. And an invariant relation is when you look at the guarded loop body, which I represent by T intersect P, where B is the function of the loop body and T is the relation that takes the pre restriction of that. So that's the representation of T as a relation then. So the invariant relation is a reflexive, transitive superset of the guarded of the function of the guarded loop body, meaning in fact it's a relation that holds between any two sets S and S prime that are separated by an arbitrary number of iterations, including zero. And why is that important? Simply because of this proposition here, which says if R is an invariant relation of W, then the function of W is a subset of R intersection. So T inverse complement, meaning R intersection condition t prime on the final state. Okay, so to compute the function of the loop, we have to find invariant relations. Take their intersection, then take the post restriction to not t, and that should deliver the the function of the loop. What are invariant relations? I know most everybody is familiar with invariant assertions and loop invariant, et cetera. We find that invariant relations are a lot more useful and a lot more powerful as a concept. So if I take this very simple program and I make it simple on purpose to be able to illustrate, these are three invariant relations. N prime equal n, obviously K less and K prime. But most importantly, F divided by K minus 1 factorial equal F prime divided by K prime minus 1 factorial. Okay? These relations hold between any two states that are separated by any number of iterations. So, yeah, there is a discussion about the relation with loop Invariance I will come back to it if there is an interest. But if I take the intersection of these three invariant relations and. I consider this precondition, which is f equal 1, k equal 1, n equal and 0, then I get this invariant relation which is n equivalent 0k greater than or equal to 1 and f equal k minus 1 factorial. So that's the loop invariant. But actually the invariant relation is saying a lot more than that. So how do we generate invariant relations? This is really the key idea is first of all we have an invariant relation that we get for free, which is this relation. And this relation says either S prime is equal to S. That's the case when no. Then when the loop does not iterate at all, or the initial state satisfies T and the final state is in the range of the guarded loop body. And for all other relations we proceed by pattern matching. And pattern matching is a situation where we look at the function of the loop body and we see if we recognize some patterns in the various clauses and depending on what we recognize, we generate corresponding invariant relation. So for example, if I have X prime equal x + a in the loop body and I know that A is non negative or actually A is positive, then what do we know? We know that X is less than X prime and that X mod A is equal to X prime mod A. Okay, if I know that X prime is X plus A and Y prime is Y plus B, what do I know? I know that ay minus bx equal AY prime minus bx prime. If I notice in the loop body X prime equal F of X and I prime = I = 1, what do I know to be invariant relation is fi of x equal fi prime of x prime, et cetera. So I recognize patterns in the code and they generate the corresponding invariant relation. I take the intersection of all this, take the post restriction to T of S prime, and then submit all that to Mathematica to get the function of the loop. So then how do we integrate this into computing the function of a program? If I have an assignment Statement x =es, we generate the following mathematical equation that says first of all, e can be evaluated at state S. So for example, if E is log, then S has to be positive. This E is a square root S has to be non negative, etc. Then XP is equal to E of S and all the other variables are preserved. That's the equation we generate for an assignment statement. If I have a sequence statement, then I take the first part of the sequence, I apply a 2m to it, whatever that will turn, it will return an equation in S sp. Then I apply a function we call sp to spp, which replaces every instance of sp by spp. Then I apply a 2m to the second term and replace every instance of S by spp. Then I quantify SPP by the existential quantifier. And what do I get? I now get an equation between S and sp. So I start with an equation between S and SP first element, an equation between S and SP second element, and I get an equation between SSP of the overall sequence. Okay? That's why you see nested calls within the Mathematica code. It's because the longer the sequence, the deeper the nesting will be. Conditional statements. It's all you know. This is very simple. If you have if ta else B, then we generate the equation ts and A to MA or not TS and A to m B. And if you have an if else. I'm sorry, if ta, then we generate the equation T of S and A to MA or not t of S and SP equals S. For the while loop. If I have a while loop, then I generate the elementary invariant relation. You remember the relation that says either the loop does not execute at all, or if the loop executes at least once, then S satisfies t and S prime is in the range of T. Enter B. So that's the one I get. Then we call INV r and ENV R is the relation that stems from the pattern matching algorithm that we described earlier with the table of recognizers and in var, we give it the condition of the loop and A to m of the loop body. Whatever A to m returns for the loop body and negation of condition t of sp. Okay? So the function of the loop body is obtained by taking the elementary invariant relation, adding all the invariant relation that stem from the recognizers, adding condition not t and having Mathematica solve in final state as a function of the initial state for loop. If I have a for loop that starts from I +1 until h I + +, then we introduce the variable I. Because remember I when you write Java code or C code or what have you, the variable of the variable that you use for the for loop is not part of the state, okay? So we quantify it existentially the initial value and the final value, and we add to that I equal 1, IP equal H plus 1 and INV R. So in R I must give it the condition of the loop and the loop body. So the condition of the loop is I less than h and the loop body is A to M of the loop body to which I add the condition IP =I +1. So approach, as you notice, is critically dependent on having recognizers that are very general. Okay? We don't want these recognizers to be to be to match only one instance. You know, we want these organizers to be as broadly applicable as possible. And we have an example of fairly generic recognizers, which are recognizers that are applicable to affine transformations. So imagine that you have a while loop that performs transformations of the form x prime equal ax plus b, where a is different from 0 and 1. Then we know that this here is an invariant relation for the loop. And this has fractional part of log base a x prime plus d divided by a minus 1 equal fractional part of the same thing for X. Also, if we have two of these, if we have two affine transformation, then this here is the invariant relation. And if instead of two I have let's say ten, then I can apply R0 the previous one to one of them, and I can apply R1 nine times to the remaining pairs composed of the pivot and each one of the nine others. Meaning what? Meaning if I have 10 affine transformations like that, I can actually generate 9 equations with r1 plus an equation with r0 plus add condition that t not T is valid for S prime. And that gives me all the necessary equations to be able to determine the function of the loop. So here is an example of what it means. Imagine that here I do x prime equal 5x plus 3. So I have a sequence Here I do y prime equal 3 y plus 5, I have the same sequence according to R0, the fractional part of all these numbers is constant. The fractional part of all these numbers is constant, as you see. And. Then the difference between the two, this is the R1, the difference is constant through the whole iteration, and using information like that will give us the function of the loop. So we have a three step algorithm for computing the function of a program. To perform the symbolic execution of the program, which is a function from initial state to final state, we are able to capture the function of iterative statements such as while loops for loops, but also other iterative statements, shutters, repeats and the like. We really owe most of the feasibility of this process to the fact that we are using two successful technologies, namely the compiler generation technology, which maps a source code into an abstract syntax tree, and the Mathematica, which then takes the equation that we generate and produce the function of the program. For the sake of comparison with existing technology. We take for example this program and we apply the invariant relation that I just showed a minute ago for affiliate transformations. And when we generate the loop invariant, we find this expression. And for comparison, we look at a tool developed at MIT several years ago called Daikon. And this is what we get with Daikon. Then we look at another tool developed at Stanford, and this is what we get for the same program. And by comparison we argue that what we are providing is a lot more precise and gives us more information. There is another tool we have been trying to run, but we couldn't develop that Princeton called srk. And we are anxious to find what SRK will deliver. So a possible critique of this approach is that we can only handle loops for which we have recognizers. But we argue that there is no way to analyze programs without producing programming knowledge, without having codifying somewhere programming knowledge and domain knowledge and recognizers are the way in which we codify this knowledge, so that the need for codifying this knowledge is a feature of the problem rather than a feature of the solution. Finally, as far as our prospects, clearly we need to define adequate database of organizers that are fairly generic. We need to also develop an algorithm for semantic matching. And it's possible that if I take a 500 line program and give you the function, you will probably find that the function is even more obnoxious than the program and it's probably harder to analyze. So then we produce functions we call assume, capture, verify, establish, which enable the user to query the source code in greater detail. And I conclude here, and I thank you for your attention.