Abstract CCured Type-Safe Retrofitting of Legacy Code
In lhis paper we propose a scheme lhai combines type in-ference and run-time checking to make exisiing C programs type saI~.}V ~ describe lhe CCured type sysiem, which ex-lends lhat of C by separaiing poinier types according to lheir usage. This type sysiem allows boih poiniers whose usage can be ve...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.134.6706 http://www.cs.virginia.edu/~weimer/p/p128-necula.pdf |
| Summary: | In lhis paper we propose a scheme lhai combines type in-ference and run-time checking to make exisiing C programs type saI~.}V ~ describe lhe CCured type sysiem, which ex-lends lhat of C by separaiing poinier types according to lheir usage. This type sysiem allows boih poiniers whose usage can be verified siaiically to be type saI>, and poiniers whose sai>ty musi be checked ai run lime.}V ~ prove a type soundness resuli and lhen we preseni a surprisingly simple type inference algoriihm lhai is able lo infer lhe appropriaie poinier kinds for exisiing C programs. Our experience wiih lhe CCured sysiem shows lhai lhe inference is very eft~ciive for many C programs, as ii is able io infer ihai most or all of the pointers are statically ver-ifiable lo be type saI>. The remaining poiniers are insiru-menied wiih efficieni run-lime checks lo ensure lhai lhey are used sai>ly. The resuliing performance loss due lo run-lime checks is 0 15056, which is several limes belier lhan com-parable approaches lhai use only dynamic checking. Using CCured we have discovered programming bugs in esiablished C programs such as several SPECINT95 benchmarks. 1 |
|---|