SpInE

SpInE is an automatic functional Specification Inference Engine for heap manipulating programs. Specifications are represented as pre and post-conditions expressed in LISF logic. The inferred specifications ensure safe execution of the program, i.e., execution without null pointer dereference, double delete etc. These specifications are inferred in a bottom-up, compositional manner, i.e., the specification of a code block or a procedure is computed from that of its component statements and independent of the execution context.
Spine analyses the input C program <program-name> and generates summaries for all functions in it. It outputs summaries in the form of Hoare triples, {P} func {Q}, for every function func in the input file. P and Q are LISF formulas. For syntax and semantics of LISF refer [2].
Spine takes two optional arguments -join -lemmas. With the option -lemma turned on, spine will utilize an extension of LISF with sub and rev predicates (refer [1]) to generate summaries. With the option -join turned on, spine will utilize sophisticated rules to generate a single summary for both the branches of the if-then-else statement.

Experimental Results

Linked List Processing Programs
Program LOC time(s) # summaries complete? Output
init 16 0.007 2 Yes init.out
delete_all 21 0.006 2 Yes delete_all.out
delete-circ 23 0.007 2 Yes delete-circ.out
delete 42 0.058 *19 No delete.out
append 23 0.010 3 Yes append.out
append-dispose 52 0.036 6 Yes append-dispose.out
copy 33 0.324 3 Yes copy.out
find 28 0.017 4 Yes find.out
insert 53 0.735 6 Yes insert.out
merge 60 0.511 12 No merge.out
reverse 20 0.012 *3 No reverse.out


Routines from firewire device driver
Program LOC time(s) # summaries complete?
BusResetRoutine 145 0.043 *3 Yes BusResetRoutine.out
CancelIrp 90 0.743 *32 Yes CancelIrp.out
SetAddressData 96 0.122 *6 Yes SetAddressData.out
GetAddressData 94 0.122 *6 Yes GetAddressData.out
PnpRemoveDevice 460 37.600 *34 No PnpRemoveDevice.out


Programs from [3,13]
Program LOC time(s) # summaries complete?
dll-reverse 23 0.084 3 No dll-reverse.out
fumble 20 0.010 2 Yes fumble.out
zip 37 0.374 4 No zip.out
nested 24 0.028 5 Yes nested.out


Use of options -lemmas (use Lemmas in strong bi-abduction) and -join (merge branches of if statement)
Program LOC time(s) # summaries complete?
reverse-reverse 30 0.025 4 No reverse-reverse.out
offset-traverse 32 0.016 1 Yes offset-traverse.out
dll-traverse-both 24 0.014 3 Yes dll-traverse-both.out
delete 42 0.082 *21 Yes delete.out
PnpRemoveDevice 460 23.800 *32 Yes PnpRemoveDevice.out

Technical reports

[1] Bhargav S. Gulavani, Supratik Chakraborty, G. Ramalingam and Aditya V. Nori, Bottum-up Shape Analysis using LISF, Technical report tr-09-31, CFDVS, IIT Bombay, December 2009 [tech-report tr-09-31]

Publications

[2] Bhargav S. Gulavani, Supratik Chakraborty, G. Ramalingam and Aditya V. Nori, Bottum-up Shape Analysis, in the Proceedings of The 16th International Static Analysis Symposium (SAS), August 2009 [ps]
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.