Topic: flavor analysis and typestates for supplementary type checking

topics > computer science > data > Group: type checking

program proving

code optimization
code optimization by flow analysis
consistency testing
debugging by usage rules
dependency analysis
immutable files and data
model checker
optimization of object-oriented programs
preventing accidental errors
race conditions
run-time assertions
safe use of pointers
safety, liveness, and system properties
static single assignment; SSA
type-safe and secure languages
weak vs. strong type checking


Typestate is a type annotation developed by Strom and Yemini for capturing initialization information. Typestate checking prevents errors due to uninitialized data. For example, if data is set in one branch, but not in another, typestate will catch this. They found this increased the locality of errors.

Winner proposed an 'unassigned' value as a generalization of NIL to explicitly make a variable dead. (cbb 1/90)

Subtopic: typestate -- type annotation up

Quote: a typestate is a type annotation that captures state attributes such as uninitialized; mutually exclusive [»stroRE1_1986]
Quote: with typestate checking can not initialize an object in only one branch of a conditional [»stroRE1_1986]
Quote: typestate captures the degree of initialization of simple and composite objects [»stroRE5_1985]
Quote: typestate information forms a lower semilattice
Quote: an operation in NIL has unique typestate preconditions and unique typestate postconditions for normal and exception exits [»stroRE5_1985]
Quote: when multiple control paths join, typestate is greatest lower bound of incoming typestates [»stroRE5_1985]
Quote: algorithm for checking typestate consistency, e.g., initialization [»stroRE1_1986]
Quote: in NIL, module definitions include typestate transitions for parameters; allowed independent development [»stroRE5_1985]
Quote: NIL's typestate interfaces meant that system testing did not reveal new errors in unit-testing; locality of errors was assured [»stroRE5_1985]
Quote: safety check of untrusted machine code by typestate analysis; allows manipulation of host data structures; checks array bounds, address alignment, initialization, null pointers, stack manipulation [»xuZ6_2000]
Quote: safety check recursive programs by using the induction-iteration method to synthesize invariant entry conditions; not implemented [»xuZ6_2000]
Quote: Vault as a safe C with execution-ordering constraints; object in one of several states; annotate functions for their effect on object state [»laruJR5_2004]
Quote: Vault identifies non-aliasing objects for type state analysis

Subtopic: design specification up

Quote: explicit specification of a procedure's design information documents the programmer's intent, allows compile-time checking, provides modularity, and enables lexical analysis and separate compilation [»rugiR4_2001]
Quote: pointer interfaces specify how procedures change the points-to information [»rugiR4_2001]
Quote: region interfaces specify the regions of memory accessed by a procedure
Quote: defining pointer and region interfaces simplified the automatic parallelization of Quicksort and other algorithms [»rugiR4_2001]

Subtopic: counterexamples & open programs up

Quote: Chord analyzes open programs and reports counterexamples; essential; detect races before deployment [»naikM6_2006]
Quote: report counterexamples for each race, categorized by field and by object; which threads, which objects, and which locks [»naikM6_2006]

Subtopic: flavor analysis -- data properties up

Quote: flavor analysis: check assumptions about data properties from assertions of those properties along all flows of control [»howdWE12_1989]
Quote: a flavor is a property of an object that changes during program execution; e.g., 'total' may be initialized, partial sum, total sum [»howdWE1_1990]
Quote: a data state expression in flavor analysis is the set of data properties that objects can have at a program location
Quote: use assumption and assertion comments to state that x has a single property or some property with other properties [»howdWE1_1990]
Quote: flavor and scheduling analysis by comment analysis on data state and operator state expressions; give assumptions and assertions [»howdWE1_1990]
Quote: input flavor statements specify data assumptions at function invocation; output statements specify data assertions at end [»howdWE1_1990]
Quote: a data state expression in flavor analysis is the set of data properties that objects can have at a program location
Quote: operator state expressions--an assumption denotes the programmer's expectation that all paths imply some operator state; an assertion becomes part of the operator state [»howdWE1_1990]
Quote: an operator state expression in scheduling analysis is the valid operator sequences that can reach a program location
Quote: an always flavor statement specifies data assumptions at every program location
Quote: the flavor analyzer does not interpret data objects; so A(T) and A(R) are treated separately [»howdWE1_1990]
Quote: flavor analysis treats task invocation and return the same as subroutine invocation and return [»howdWE1_1990]
Quote: handle infeasible paths by assigning flavors to a special 'path condition'; stop path exploration when the flavor assumption fails [»howdWE1_1990]
Quote: flavor analysis enormously useful for checking assumptions about temporaries and registers; particularly for maintenance [»howdWE12_1989]
Quote: used flavor analysis on an existing 70K assembly language program; effective for tracking registers and temporary variables [»howdWE1_1990]

Subtopic: path analysis up

Quote: PREfix for path-by-path analysis across function boundaries; finds null pointers, improper memory allocation/deallocation; uninitialized variables, resource state errors, improper library usage [»laruJR5_2004]

Subtopic: pointer analysis up

Quote: CCured identifies safe pointers, sequence pointers that require bounds check, and wild pointers that require a type checks [»necuGC5_2005]
Quote: CCured identifies forward sequence pointers and other pointer kinds [»necuGC5_2005]

Subtopic: type guard, proper usage up

Quote: Vault defines type guards for specifying resource management protocols; e.g., operations performed in a valid order, operations required before access, operations that will be performed; enforced at compile time [»deliR6_2001]
Quote: a type specifies the valid operations while a type guard specifies when an operation is valid
Quote: a type guard consists of a key and optional local state; the key must be in the global held-key state when accessing the variable [»deliR6_2001]
Quote: Vault's type system is based on Capability Calculus and alias types [»deliR6_2001]

Subtopic: annotation up

Quote: fix security warnings or add annotations; run Splint until done [»evanD1_2002]
Quote: annotations and static analysis identified format bugs, buffer overflow bugs, and unknown flaws in wu-ftpd [»evanD1_2002]
Quote: use annotations for static analysis of properties such as not-null or unique-reference [»evanD1_2002]
Quote: use 'confine' and 'restrict' to track lock state; removed spurious type errors in 138 of 152 device driver modules [»aikeA6_2003]
Quote: read-only should be the default type annotation [»tschMS10_2005]

Subtopic: field property up

Quote: field properties refine type information for reference fields; e.g., does not reference subclasses of C, contains fixed-size array [»ghemS6_2000]
Quote: implement field analysis with static, single-assignment (SSA) graph; analyze loads and stores without optimization or context-sensitive information [»ghemS6_2000]
Quote: field analysis in linear time by code size; 10% cost; 7% faster
Quote: a field inherits its assignability and mutability from the field's references; mutability is transitive by default [»tschMS10_2005]
Quote: Javari guarantees that a read-only reference cannot be used to reassign any field in the object's protected, abstract state [»tschMS10_2005]

Subtopic: memory region annotation up

Quote: use annotations to track memory regions across function calls
Quote: avoid memory errors by partitioning memory into pools according to the points-to graph; allows aggressive interprocedural pointer analysis; only 10% overhead due to static checking [»dhurD6_2006]
Quote: detect invalid references by partitioning memory according to its points-to graph; homogeneous pools avoid dangling pointers and run-time checks [»dhurD6_2006]

Subtopic: annotation for race detection up

Quote: type annotation for static race detection; found errors in Java libraries; 20 annotations per 1000 lines [»flanC6_2000]
Quote: type annotations--'guarded_by lock' for fields and 'requires lock_list' for methods; 1000 lines per programmer hour [»flanC6_2000]
Quote: use Flanagan and Abadi's race-free type system to prove that Guava objects are never concurrently accessed [»bacoDF10_2000]
Quote: Chord uses annotations to specify which threads can not execute in parallel; 42 annotations per 1.5 million lines of code [»naikM6_2006]

Subtopic: unassigned, uninitialized up

Quote: can have a value 'unassigned' that makes a variable uninitialized [»winnRI10_1984]
Quote: run-time checks of actual types; unallocated, uninitialized, integral, real, and pointer; shows exact location of errors; 20x slower [»logiA4_2001]

Subtopic: array bounds up

Quote: efficient array bound checking across procedure calls; reports name and dimension of erroneous array; uses source-to-source Fortran compiler and convex array regions [»nguyTV5_2005]
Quote: symbolic bounds analysis for static race detection, automatic parallelization, array bounds analysis, size of computed values; determines upper and lower bounds for array indices and pointers [»rugiR3_2005]

Subtopic: mirror of memory up

Quote: store run-time type information in a mirror of memory, 4 bits/byte; continuation bit, type, and size; two nibbles identifies an object [»logiA4_2001]

Subtopic: examples up

Quote: CSSV for static analysis of buffer overflows in C; optional contract per procedure reduces to integer expressions; handles heap allocation, multi-level arrays, function pointers, casting; faster than authors' previous algorithm [»dorN6_2003]

Subtopic: limitations of type analysis up

Quote: avoid using annotations to guide the constraint solver; error-prone [»zandBT11_2005]
Quote: use static analysis, symbolic interpretation, reachability, and logic model checking for non-deterministic software; but bugs will still remain
Quote: limitations of safety check -- does not work for local arrays, multiple array-typed fields, array references, subclasses, non-linear constraints [»xuZ6_2000]
Quote: induction-iteration for typestate, safety checking can not detect array errors if correctness depends on values outside of the loop

Related Topics up

Group: program proving   (10 topics, 311 quotes)
Group: security   (23 topics, 874 quotes)

Topic: code optimization (54 items)
Topic: code optimization by flow analysis (47 items)
Topic: consistency testing (60 items)
Topic: debugging by usage rules (41 items)
Topic: dependency analysis (34 items)
Topic: immutable files and data (59 items)
Topic: model checker (49 items)
Topic: optimization of object-oriented programs (16 items)
Topic: preventing accidental errors (37 items)
Topic: race conditions (33 items)
Topic: run-time assertions (25 items)
Topic: safe use of pointers (102 items)
Topic: safety, liveness, and system properties (22 items)
Topic: static single assignment; SSA (19 items)
Topic: type-safe and secure languages (43 items)
Topic: weak vs. strong type checking
(42 items)

Updated barberCB 11/05
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.