Hello. Welcome to this lecture on Static Program Analysis. It's reasoning about a program without executing the program. So, here is an example to start with. A simple algorithm to compute the greatest common divisor of two numbers. It's the standard Euclidean algorithm you go through the pair of numbers dividing the bigger one by the smaller one, take the remainder, throw away the bigger one, and keep repeating until you come to 0. So, if we run the program with a couple of inputs, let us say, we give 36 and 15 as the inputs, we divide 36 by 15 we get a remainder of 6, throw away 36 now we work with 15 and 6, we get 3 and so on, and eventually we get to 3 and 0. The non-zero number, in this case 3, happens to be the GCD of the two numbers. So, we return the value 3 as the answer. Great, we executed the program for a couple of inputs and we saw the output, this is what we do in testing. When we write a new program, we give certain inputs and see if it produces the expected output. But just because you ran it for a bunch of inputs and saw the expected outputs does it mean that the program is right? What if this loop never terminates? Are we sure that the divisor will always reach 0? Is it possible that you get a divide-by-zero error. You are dividing the dividend by the divisor, can the divisor be an error of 0 when you do this division operation? A little more involved is the question of whether GCD would always return a positive number or will it ever return a negative number? By definition, GCD has to be positive. So, these are legitimate questions that one may ask about a program that we write. To answer these questions, we need to analyze the program for all possible inputs, and that is where static analysis comes in. You analyze a program to answer questions about its behavior, and its static in the sense that you don't execute the program, you reason about its execution for all possible paths through the program. Examine what a program would do and analyze what it would do for any given input. So, this is what compilers typically do when they try to optimize a program when they compile source code to object code. They move code, remove variables and so on and when they do that, they had to be sure that such transformations do not affect the semantics of the program, so some analysis has to happen. So, this is in contrast to dynamic analysis where you run the program and reason about what you saw during that execution. This is what we typically do when we execute test cases, we run a program for some given input and see its output, and see its execution phase, and see if all the things that the program did during the execution is right or wrong. So, in general, you can postulate the problem as follows. Does a program, given program P, satisfy the property phi? So, you want an analyzer, a static analyzer which is some kind of a program. Again, it's an algorithm that takes an input program and a property of interest and gives an answer of yes, this satisfies this property or no, this program doesn't satisfy the property. The kinds of properties one would be interested in when analyzing programs are things like no infinite looping behavior. I don't want the program to run forever, no divide-by-zero exception, or no buffer-overflow, or no null-pointer exceptions. These are the kinds of things that we would want to check our program for. The benefit of doing such analysis is that it can establish program properties for all possible executions. So, we can think of it in the following manner; think of its jagged star as representing a set of elements points and each point in this set is a possible program state. By program state we mean a specific assignment of values to the variables in the program. So, these are all the possible configurations that the program could get into. So, what we are trying to see is, does this set fall inside the set of all possible configurations where the property holds? In other words, is the set of reachable states of the program your subset of the set of states where the property of interest holds. If this relationship holds, then we can say that the program has the desired property. The advantage of doing such an analysis, is that you can detect really hard to detect faults otherwise. Let say there is a reachable set of states of the program and here is the set of states where the property holds and by this analysis, we find that there is some corner in this reachable state space where there is a bug, that is a reachable state of the program, but it is outside the set of states where the property holds maybe that's where a null-pointer exception happens or maybe that sort of buffer-overflow happens. So, to sum up, static analysis can establish a property for all possible executions of a program. For example, you can reason in this GCD function that there is no divide-by-zero error, by looking at all possible paths that lead to the division operation and checking whether the divisor is actually 0 or not. You can produce an explanation for why a property may not hold, and this is actually a more useful benefit of doing this analysis. When something fails, you run a test case and it fails, you have to often go back and look at the program and try to figure out why something happened. But the power of analysis is that in the process of figuring out where a property fails, the analyzer would have figured out a path, an execution sequence to get to that point and that becomes an immediate test case or an immediate execution trace that shows you how the property might be violated. For example in this case, you may see that an analyzer produces something like a GCD of negative 1 and negative 1 returns negative 1 as its value. So, that is because of how the division and modular operations work with integers in typical architectures. So, we can also detect faults that are hard to detect by testing the program. Say you have multithreaded programs, accessing shared data, and different threads access the data in different orders and sometimes you may have rare race conditions. You may find a bug only when thread 1 writes something and then thread 2 reads something before thread 1 writes another value and that may not happen when you actually run a test case because from each one run to another run, the execution sequence may differ whereas by analysis, we can figure out that there is a possible execution sequence where this rare bug manifests. So if it's all such nice and wonderful, why not always use static analysis. That becomes a fundamental limitation of static analysis. That is the theoretical limitation which says that, non-trivial semantic properties of programs are really undecidable. What does it mean to say non-trivial semantic properties? If you have some programs which satisfy the property and some programs that do not satisfy the property, what this result says is you cannot have an effective procedure or an algorithm that can distinguish between the programs that have the property and the programs that do not have the property. So this is a consequence of what's called Rice's theorem in computability theory. So, if that's the case, what do we do? The practical consequence of this is that you cannot have a precise algorithm that exactly identifies those programs that have the property and those that doesn't. So, we have to work with approximations. So, typically these analyses were by approximating in one direction or the other. Instead of taking the exact reachable states of the program, you compute an approximation of the reachable states and it can be an overapproximation or an underapproximation. If it's an overapproximation, the analysis will be sound because if the property holds for the approximation, then it will hold for the program. So, if you approximate the set of reachable states and and it's an over approximation and you claim that for this overapproximation the analysis figures there is no null-pointer exception, you can be sure that the actual program doesn't cause a null-pointer exception. On the other hand, if you underapproximate, the property will hold for the program then the property holds for the approximation too, in which case the analysis will be complete. So, whenever it says the property holds, it really holds for the program. If it's sound, and in the case of completeness, if the analysis says that the property doesn't hold, then you can be sure that it doesn't hold for the program. The consequence of Rice's theorem is that you have to essentially work with some approximation like this. You cannot have exact effective procedure. With approximations we can still establish program properties, right. You have a reachable set of states of the program, you compute an overapproximation and check whether the overapproximation fits within the set of reachable states and if it does, we can declare that the program does have the property. But of course it can also detect rare faults. If you again do this approximation and find your portion of the approximation doesn't fit inside the actual set of states where the property holds, it may be able to show you your path to this fault. But on the other hand, we can always have this problem of ending up with spurious faults. So we do this same analysis and you may not actually find the real bug you may find a false alarm. Much of the static analysis techniques dealing with this false alarm is a big issue. If we want the analysis to scale and be fast and be efficient, we have to do coarser and coarser approximations which means we'll have more and more false alarms and that will mean there are real faults and it can even drown out the actual faults and if the false alarms are too many, then it comes to the point of being useless because you will be dealing with false alarms all the time. So there are limitations of static analysis. Typically, you conservatively approximate to check for the desired property. Some programs with the desired property would still be rejected, for example a Java compiler check for variable-initialization-before-use which is standard can at times flag some programs as violating the property even if in reality such a path is not possible during execution. We have to deal with these false alarms which are the result of too conservative of an approximation. To compare testing with static analysis, testing can only show the presence of defects not their absence. But a static analysis may be able to establish the absence of whole classes of errors that's where the power comes in. On the other hand, testing can be performed at scale on whole systems. The big issue with any analysis is that as you scale the analysis for larger and larger and more complex programs, you would have to compromise somewhere typically introducing more inprecision, more approximation. And testing, you can think of it as being optimistically inaccurate. You run a set of test cases and if all those test cases pass, we say okay the program is good to release which means you may actually release a program that has some faults. On the other hand, static analysis is typically pessimistically inaccurate. It may lead to the rejection of correct programs. So if you overapproximate the set of reachable states and that overapproximation doesn't fit in the set of states that the property holds, you are going to reject and that rejection may be based on this false alarm. So, to sum up, static analysis is a powerful technique that should complement testing. It can help in ruling out a whole class of errors. In the following lectures, we will see how to use some tools that do various static analysis.
