View source for Shape analysis (program analysis)

In [[Program analysis|program analysis]], '''shape analysis''' is a static code analysis technique that discovers and verifies properties of [[Linker (computing)|linked]], dynamically allocated data structures in (usually [[Imperative programming|imperative]]) computer programs. It is typically used at compile time to find software bugs or to verify high-level correctness properties of programs. In [[Java (programming language)|Java]] programs, it can be used to ensure that a sort method correctly sorts a list. For C programs, it might look for places where a block of memory is not properly freed.

==Applications==

Shape analysis has been applied to a variety of problems:
* Memory safety: finding [[Memory leak|memory leak]]s, dereferences of [[Dangling pointer|dangling pointer]]s, and discovering cases where a block of memory is freed more than once.<ref>{{Cite book|chapter-url = https://link.springer.com/content/pdf/10.1007/3-540-45306-7_10.pdf|doi = 10.1007/3-540-45306-7_10|chapter = Interprocedural Shape Analysis for Recursive Programs|title = Compiler Construction|volume = 2027|pages = [https://archive.org/details/compilerconstruc0000cc20/page/133 133–149]|series = Lecture Notes in Computer Science|year = 2001|last1 = Rinetzky|first1 = Noam|last2 = Sagiv|first2 = Mooly|isbn = 978-3-540-41861-0|url = https://archive.org/details/compilerconstruc0000cc20/page/133}}</ref><ref name="Be07">{{Cite book | chapter-url=https://link.springer.com/content/pdf/10.1007/978-3-540-73368-3_22.pdf |doi = 10.1007/978-3-540-73368-3_22|chapter = Shape Analysis for Composite Data Structures|title = Computer Aided Verification|volume = 4590|pages = 178–192|series = Lecture Notes in Computer Science|year = 2007|last1 = Berdine|first1 = Josh|last2 = Calcagno|first2 = Cristiano|last3 = Cook|first3 = Byron|last4 = Distefano|first4 = Dino|last5 = o'Hearn|first5 = Peter W.|last6 = Wies|first6 = Thomas|last7 = Yang|first7 = Hongseok|isbn = 978-3-540-73367-6}}</ref>
* Finding array out-of-bounds errors{{citation needed|date=November 2012}}
* Checking [[Typestate analysis|type-state properties]] (for example, ensuring that a file is <code>open()</code> before it is <code>read()</code>){{citation needed|date=November 2012}}
* Ensuring that a method to reverse a linked list does not introduce cycles into the list<ref name="Be07"/>
* Verifying that a sort method returns a result that is in sorted order{{citation needed|date=November 2012}}

==Example==

Shape analysis is a form of [[Pointer analysis|pointer analysis]], although it is more precise than typical pointer analysis. Pointer analysis attempts to determine the set of objects to which a pointer can point (called the points-to set of the pointer). Unfortunately, these analysis are necessarily approximate (since a perfectly precise static analysis could solve the [[Halting problem|halting problem]]). Shape analysis can determine smaller (more precise) points-to sets.

Consider the following simple C++ program.
<source lang="cpp">
Item *items[10];
for (int i = 0; i < 10; ++i) {
    items[i] = new Item(...); // line [1]
}
process_items(items); // line [2]
for (int i = 0; i < 10; ++i) {
    delete items[i]; // line [3]
}
</source>

This program builds an array of objects, processes them in some arbitrary way, and then deletes them. Assuming that the <code>process_items</code> function is free of errors, it is clear that the program is safe: it never references freed memory, and it deletes all the objects that it has constructed.

Unfortunately, most pointer analyses have difficulty analyzing this program precisely. In order to determine points-to sets, a pointer analysis must be able to ''name'' a program's objects. In general, programs can allocate an unbounded number of objects; but in order to terminate, a pointer analysis can only use a finite set of names. A typical approximation is to give all the objects allocated on a given line of the program the same name. In the example above, all the objects constructed at line [1] would have the same name. Therefore, when the <code>delete</code> statement is analyzed for the first time, the analysis determines that one of the objects named [1] is being deleted. The second time the statement is analyzed (since it is in a loop) the analysis warns of a possible error: since it is unable to distinguish the objects in the array, it may be that the second <code>delete</code> is deleting the same object as the first <code>delete</code>. This warning is spurious, and the goal of shape analysis is to avoid such warnings.

==Summarization and materialization==

Shape analysis overcomes the problems of pointer analysis by using a more flexible naming system for objects. Rather than giving an object the same name throughout a program, objects can change names depending on the program's actions. Sometimes, several distinct objects with different names may be ''summarized,'' or merged, so that they have the same name. Then, when a summarized object is about to be used by the program, it can be ''materialized''—that is, the summarized object is split into two objects with distinct names, one representing a single object and the other representing the remaining summarized objects. The basic heuristic of shape analysis is that objects that are being used by the program are represented using unique materialized objects, while objects not in use are summarized.

The array of objects in the example above is summarized in separate ways at lines [1], [2], and [3]. At line [1], the array has been only partly constructed. The array elements 0..i-1 contain constructed objects. The array element i is about to be constructed, and the following elements are uninitialized. Shape analysis can approximate this situation using a summary for the first set of elements, a materialized memory location for element i, and a summary for the remaining uninitialized locations, as follows:

{| border="1" align="center" cellspacing="0" cellpadding="3"
|- align="center"
| 0 .. i-1
| i
| i+1 .. 9
|-
| pointer to constructed object (summary)
| uninitialized
| uninitialized (summary)
|}

After the loop terminates, at line [2], there is no need to keep anything materialized. The shape analysis determines at this point that all the array elements have been initialized:

{| border="1" align="center" cellspacing="0" cellpadding="3"
|- align="center"
| 0 .. 9
|-
| pointer to constructed object (summary)
|}

At line [3], however, the array element <code>i</code> is in use again. Therefore, the analysis splits the array into three segments as in line [1]. This time, though, the first segment before <code>i</code> has been deleted, and the remaining elements are still valid (assuming the <code>delete</code> statement hasn't executed yet).

{| border="1" align="center" cellspacing="0" cellpadding="3"
|- align="center"
| 0 .. i-1
| i
| i+1 .. 9
|-
| free (summary)
| pointer to constructed object
| pointer to constructed object (summary)
|}

Notice that in this case, the analysis recognizes that the pointer at index <code>i</code> has not been deleted yet. Therefore, it doesn't warn of a double deletion.

==See also==
* [[Alias analysis]]
* [[Escape analysis]]

==References==
{{reflist}}

==Bibliography==

*{{cite book
  | author = Neil D. Jones
  | pages = 66–74
  | publisher = ACM
  | year = 1982
  | doi = 10.1145/582153.582161
  | isbn = 0897910656
  |s2cid=13266723 }}

*{{cite journal
  | author1 = Mooly Sagiv
  | author2 = Thomas Reps
 | author3 = Reinhard Wilhelm
  | title = Parametric shape analysis via 3-valued logic
  | journal = ACM Transactions on Programming Languages and Systems
  | volume = 24
  | issue = 3
  | pages = 217&ndash;298
  | publisher = ACM
  | date = May 2002
  | url = http://www.cs.wisc.edu/wpis/papers/toplas02.pdf
  | doi = 10.1145/292540.292552
  | citeseerx = 10.1.1.147.2132
  | s2cid = 101653
 }}

*{{cite book
  | last1=Wilhelm
  | first1=Reinhard
  | last2=Sagiv
  | first2=Mooly
  | last3=Reps
  | first3=Thomas
  | editor1-first=Y. N.
  | editor1-last=Srikant
  | editor2-first=Priti
  | editor2-last=Shankar
  | title=The Compiler Design Handbook: Optimizations and Machine Code Generation, Second Edition
  | publisher=CRC Press
  | date=2007
  | pages=12–1–12–44
  | chapter=Chapter 12: Shape Analysis and Applications
  | isbn=978-1-4200-4382-2 }}

{{Compiler optimizations}}

[[Category:Static program analysis]]

{{Sourceattribution|Shape analysis (program analysis)}}