CSE503: Software Engineering
Lecture 22 (March 1, 1999)

David Notkin

v LCLint [Evans et al.]

Ø [Material taken in part from a talk by S. Garland]

Ø Add some partial specification information to C code to

Ø Detect potential bugs

Ø Enforce coding style

v Versatile and lightweight

Ø Incremental gain for incremental effort

Ø Fits in with other tools

Ø Detects potential bugs

Ø Specifications enable more accurate checks, messages

Ø Memory management a particular problem in the C language

Ø Enforces coding style

Ø Abstraction boundaries

Ø Use of mutable and immutable types

v LCLint Does Not

Ø Encourage programmer to write

§ Contorted code

§ Inefficient code

Ø Report only actual errors

Ø Report all errors

Ø Insist on reporting a fixed set of potential errors

§ Many options and control flags

v Ex: Definition before Use

Ø Sample code
if (setVal(n, &buffer)) ...

Ø Must buffer be defined before calling setVal?

§ Yes: bool setVal(int d, char *val);

§ No: bool setVal(int d, out char *val);

Ø Is buffer defined afterwards?

§ Yes: bool setVal(...); {modifies *val;}

§ Maybe: bool setVal(...); {modifies nothing;}

§ NO!: bool setVal(...); {ensures trashed(val);}

v More Accurate Checks

Ø Conventional lint tools report

§ Too many spurious errors

§ Too few actual errors

Ø Because

§ Code does not reveal the programmer’s intent

§ Fast checks require simplifying assumptions

§ Specifications give good simplifying assumptions

v Abstraction Boundaries

Ø Client code should rely only on specifications

Ø Types can be specified as abstract

§ immutable type date;
date nextDay(date d); { }
mutable type set;
void merge(set s, set t); {modifies s;}

v LCLint detects

Ø Inappropriate access to representation

Ø Including use of ==

v Checking Abstract Types

Ø Specification: set.lcl contains the single line
mutable type set;

Ø Client code
#include "set.h"
bool f(set s, set t) {
if (s->size > 0) return (s == t);
...

Ø > lclint set client.c
client.c:4,7: Arrow access field of abstract type (set): s->size
client.c:5,13: Operands of == are abstract type (set): s == t

v Checking Side Effects

Ø Specification:
void set_insert (set s, int e)
{ modifies s;}
void set_union(set s, set t)
{ modifies s;}

Ø Code (in set.c) :
void set_union (set s, set t) {
int i;
for (i = 0; i < s->size; i++)
set_insert(t, s->elements[i]);
}

Ø Message:
set.c:35, 27: Called procedure set_insert may modify t:
set_insert(t, s->elements[i])

v Checking Use of Memory

Ø Specifications

only char *gname;
. . .
void setName (temp char *pname) char *gname;

Ø Code
void setName (char *pname) {
gname = pname;
}

Ø LCLint error messages
sample.c:2:3: Only storage gname not released before assignment: gname = pname
sample.c:2:3: Temp storage assigned to only: gname = pname

v If C Were Better...

Ø Would LCLint still help?

Ø Yes, because specifications

§ contain information not in code

§ contain information that is hard to infer from code

§ are usable with legacy code, existing compilers

§ can be written faster than languages can be changed

§ are important even with better languages

v Experience with LCLint

Ø Reliable and efficient

Ø Runs at compiler speed

Ø Used on both new and legacy code

Ø 1,000-200,000 line programs

Ø Over 500 users have sent e-mail to MIT

Ø Tested with varying amounts of specification

Ø Lots to almost none

Ø LCLint approximates missing specifications

Ø Results encouraging

v Understanding Legacy Code

Ø Analyzed interpreter (quake) built at DEC SRC

Ø Discovered latent bugs (ordinary lint can do this)

Ø Discovered programming conventions

Ø Documented use of built-in types (int, char, bool)

Ø Identified (and repaired) (nearly) abstract types

Ø Documented action of procedures

Ø Use of global information, side-effects

Ø Enhanced documentation a common thread

Ø Easier to read and write because formulaic

Ø More trustworthy because checked

v Fundamental benefit

Ø Partial specifications

Ø Low entry cost

Ø You get what you pay for (or maybe a bit more)

v Purify

Ø Dynamic (commercial) tool for detecting memory leaks and access errors; there are others, such as Bounds Checker

§ http://www.rational.com/products/purify/

Ø In some sense, a dynamic analog to the memory checking aspects of LCLint

v Trapping every memory access would be overly expensive

Ø Purify inserts function calls before loads and stores to maintain a table that holds a 2-bit state for each byte in the heap and stack

Ø Requires working with malloc/free, too

v Memory State Transitions

Ø Writing to memory with any bytes that are unwriteable prints a diagnostic

Ø Same with reading unreadable bytes

v Other violations

Ø Array Bound Violations

§ Allocate a “red-zone” around malloc blocks, recording them as unwriteable and unreadable

Ø Uninitialized variables

§ Initialize them to allocated-but-uninitialized state

Ø Accessing freed memory

§ Do not reallocate memory until it has aged

§ Aging can be specified by the user in terms of number of calls to free

v Overhead

Ø 2 bits per state; about 25% memory overhead during development

Ø Run-time no worse than 5.5 times optimized C code (and usually no worse than compiling with debugging on)