Solving Shape-Analysis Problems with Languages with Destructive updatingIntroductionShape AnalysisNew AlgorithmThe is# (is shared) variableis# ExerciseSlide 7Slide 8ExampleIteration 1Iteration 1 (Continued)Iteration 2Iteration 2 (Continued)Iteration 3Iteration 3 (Continued)Iteration 4Iteration 4 (Continued)Tracking and Aliasing FunctionsNode MaterializationCutting the ListNormalizationShape Graphs – Basic TerminologyConcrete Semantic OperationsDeterministic (DSG) vs. Nondeterministic Shape Graphs (SSG)Slide 25Concrete SemanticsAbstract Semantics – Static Shape-Graphs (Definition 5.1.1)Join Operation ( ) (Definition 5.1.2)Abstract Semantics – The Abstraction Function (Definition 5.2.1)Abstract Semantics – The Abstraction Function (Definition 5.2.1)Slide 31Slide 32iis function (induced is-shared)ConcretizationExamples (Abstract Semantics)Abstract InterpretationConcrete PredicatesStrong NullificationIf-Then-ElseMerging of Two ListsMerging of Two Lists - normalizedInconsistenciesExtensionsReducing the Number of Shape-NodesWideningNarrowingRefining Concrete SemanticsMay Alias-ProblemPossible EnhancementsInsertion into a ListThe EndSolving Shape-Analysis Problems with Languages with Destructive updatingBy M. Sagiv et al.Presentation byJustin BronnTravis PinneyJosh BaumanIntroductionAddresses problems with pointer, alias, sharing, and storage analysis, and type-checking problems.Storage analysis is emphasized.Shape AnalysisGive a conservative, finite characterization of the possible “shapes” that a programs heap-allocated data structures can have at each program pointNew AlgorithmVerifies shape-preservation properties of lists, trees, and certain programs that update circular lists.Differences from Previous methods: Deliberately drops information about concrete locations. Run-time locations that are not pointed by variables are clustered in a single summary node.Removes edges on the tail of lists.Sharing through variables: When two variables point to the same cons cell – it is represented directly by shape-graph edges.The is# (is shared) variableEach SG# (Static-Shaped Graph) has a boolean value associated with it {false, true}.When true, it indicates the cons-cells represented by n may be the target of pointers emanating from two or more distinct cons-cell fields.is# ExerciseWhat is the is# value of this graph?is# ExerciseWhat is the is# value of this graph?is# ExerciseWhat is the is# value of this graph?ExampleUses a program that performs a list reversal via destructive updating.Invariant is something that does not change. In the program reverse(x,y) these always hold true1. Variable x points to an unshared, acyclic, singly linked list.2. Variable y points to an unshared, acyclic, singly linked list, and t may point to the second element of the y-list (if such an element exists).3. The lists pointed to by x and y are disjointIteration 1Iteration 1 (Continued)Iteration 2Iteration 2 (Continued)Iteration 3Iteration 3 (Continued)Iteration 4Iteration 4 (Continued)Tracking and Aliasing Functions “t:=y” Tracking the aliasing of configurations using “names” attached to shape-nodes. Liquidization and RenamingLiquidizing, when a variable t no longer points to a cons-cell, we remove the t from the name of n{t}This is done because the “name” of the shape-node goes into phi (falls into the primordial soup)Renaming occurs when a statement is processed that can increase the amount of sharing in a concrete store.Ex: “y := x” | n{t,y} -> n{t}| n{x} -> n{y,x}The use of sets of variables to name the nodes in SSGs can result in an exponential number of shape-nodes. Techniques to sidestep this problem is discussed in the Optimization section (Section 2.2)Node Materialization When x := x.cdr occurs, the affect has been to “materialize” a new non-summary from n-phi. This materialization conservatively covers all possible configurations of the storage.Cutting the List“y.cdr := t” cuts the y list at the head, (produces the fifth SSG from the fourth SSG}The cdr edge of shape-node n{y} is first removed. This cuts the y list at the head, seperating the first element n{y}, from the tail, which x points to.A cdr edge from n{y} to n{t} is then added, which concatenates shape-node n{y} at the head of the list that t points to.NormalizationOnly one constructor or selector is applied per assignment statementA selector is something like x.car or x.cdrAn expression cons(x,y) is executed in three steps1. An unitialized cons cell is allocated, and its address is assigned into a new temp variable2. The car component of the temp is initialized with the value of x 3. The cdr component of temp is initialized with a value of yAll allocation statements must be in the form x := new, you can’t use x.sel := new!!! Each assignment statement, the same variable cannot occur on the left and right hand sideEach assignment of the form lhs:=rhs in which rhs ==/ nil is An assignment statement of the form temp := nil is placed at the end of the program for each temporary variable introduced in the normalization.Shape Graphs – Basic TerminologyEv is defined as the graph’s set of variable edges: From the start to the first node. It is denoted [x,n] where x is a pointer variable (PVar) and n is a shape node.Es is defined as the graph’s set of selector edges: Between nodes. It is denoted <s, sel, t> where s and t are the shape-nodes and sel is of the set {car, cdr}When Ev(x) is overloaded, it represents When Es(s, sel) is overloaded, it represents In concrete semantics, the result of an execution sequence is a shape-graph that represents the state of heap-allocated storage in memory.Concrete Semantic Operations1. Variable Edge  Null2. Selector Edge  Null3. Variable Edge  New4. Variable Edge  Variable Edge5. Selector Edge  Variable Edge6. Variable Edge  Selector EdgeDeterministic (DSG) vs. Nondeterministic Shape Graphs (SSG)Deterministic Shape Graphs (DSG):Deterministic (DSG) vs. Nondeterministic Shape Graphs (SSG)Nondeterministic Shape Graph (SSG):Concrete SemanticsNonstandard in the following ways1. The only parts of the store that the concrete semantics keeps track of are the pointer variables and the cons-cells of heap-allocated storage.2. Rather than causing an “abnormal termination” of the program, dereferences of nil pointers and