cXprop

cXprop

News Overview Readme Mailing list Downloads Installation Use Publications Links

News

3/13/08 - Added pdf versions of powerpoint slides, and added a lecture I gave about cXprop a year ago. I believe I had not put it on the web prior to this because RAM compression was under anonymous review at that time.
1/21/08 - John Regehr presented a talk about cXprop. This month I have been setting up and running analyses for the purpose of evaluation. This talk includes a taste of that information. You can find it here.
12/13/07 - The new version of cXprop is up and running, and this page has been updated here and there to reflect changes I have made. Please email me with complaints, comments, and suggestions!
12/13/07 - John Regehr was running cXprop for native applications last night (as opposed to AVR or msp430 MCUs) and found some weird behavior. Turns out that when I wrote the 8051 machine dependency stuff I accidentally wrote over the native machine dependency file. That has been fixed, and I am about to do an update to this site. The way cXprop is configured has also been chaned, which is why a more substantial update is necessary. It should be up in the next hour or two (right now it is almost 10:00 am MST). Until I post another news item, though, things might be "in transit."
11/20/07 - John Regehr gave a talk about where cXprop is and where it is going during the next year. I posted it here.
11/16/07 - I updated the cil-cXprop.tgz download on the CComp page again. A handful of people have been wanting cXprop to dump its state at the end of an analysis. The --cxp_global_states flag in this version does that.
11/13/07 - I updated the cil-cXprop.tgz download on the CComp page to our current version. This takes care of some compile problems people on newer linux distributions are having
04/27/07 - I created a page for CIL Tools for TinyOS that is a collection of binaries, scripts, and instructions designed to make getting started with our tools easier. That includes cXprop
04/26/07 - My most recent extension of this work has been CComp. That tool builds off of cXprop, so you might want to poke around there. As usual, feel free to email me if you have any questions.
09/29/06 - Put a little note saying to email me for latest source or if you have any questions.
08/22/06 - Took down "beta" version I threw up for LCTES. Updated "non-beta" version to be whatever is in CVS right now. Updating contents for current behavior of cXprop. I tested the installation instructions and it seems to work fine.
06/12/06 - Threw up a "beta" version of cXprop. This version has been significantly changed and includes some new features. The changes are pervasive. I describe what has happened in general, but for specifics you will have to email me directly.
04/25/06 - Major update to the web page. Created a publications section, a complete CIL installation with cXprop already included (for easier installation), updated instructions, and some other changes.
02/13/06 - Updated web page. You can now get the current version (as of today) of cXprop and I think the installation instructions are correct. Of course, feedback is appreciated.
02/09/06 - I have not updated this web page since September, and even then it was pretty shabby. It is mostly just a stub right now. The version of cXprop that can be downloaded here is old and not very effective. Plus, the installation instructions are untested. However, if you send me an email I would be happy to send you cXprop and help you get it up and running as an extension to your CIL installation. I am sorry I have not update the page yet, but it has been a busy couple of weeks. I hope to update the page soon (within a week). Feel free to join the mailing list while you are waiting!
09/07/05 - If you are an extremely motivated seminar student, then you looked up the web page at the back of my paper and came here. Sorry there is not much here. If you want to get cXprop running on your machine, follow the instruction. If you have problems, just stop by my office or sent me an email. I am in 2172 MEB .

Top

Overview

Many abstract value domains such as intervals, bitwise, constants, and value-sets have been developed to support dataflow analysis. Different domains offer alternative tradeoffs between analysis speed and precision. Furthermore, some domains are a better match for certain kinds of code than others. cXprop is an analysis and transformation tool for C that implements "conditional X propagation," a generalization of the well-known conditional constant propagation algorithm where X is an abstract value domain supplied by the user. cXprop is interprocedural, context-insensitive, and achieves reasonable precision on pointer-rich codes. We have applied cXprop to sensor network programs running on TinyOS as well as more general C programs. Our analysis of global variables is supported by a novel concurrency model for interrupt-driven software.

cXprop was created by Nathan Cooprider and John Regehr. It is maintained by Nathan Cooprider.

We are actively working on improving cXprop in the following four ways:

  • Improving analysis speed
  • Improving precision
  • Improving expressiveness
  • Finding more nails to hit

If you have questions or want the most current version of cXprop, please email Nathan Cooprider at coopATcsDOTutahDOTedu.


Please note that the actual relationship of the modules has become a bit more confusing and messy since this figure was first made, but the abstract domain interface is still fairly clean

Top

Readme

The documentation for cXprop is less-than stellar. Part of this can be blamed on the fact that it started out as a simple CIL extension that was just being written just to test Usit's transfer functions. As it grew and evolved, features were added and modified with this same mind-frame. By the time it became clear that cXprop was something that would stand on its own, the documentation process was yet to be started.

However, I believe those who have given cXprop a chance have found me willing and able to help. I try to provide quick support and would love to get you off and running. cXprop is a really cool tool and we find it very useful. I expect that sooner or later more people will discover this secret and then I will have to write some more documentation. In the meantime, I will write documentation as necessary based on user feedback.

Top

Mailing list

The mailing list cXprop-users for cXprop is hosted at Google. To subscribe, enter your email address below; you will be sent a confirmation by email.

Google Groups cXprop-users at googlegroups.com
Email:
Browse Archives

Top

Downloads

General

cXprop

Top

Installation

Please let us know about any problems you have during the installation or any parts of the process which are confusing. This manual is a work in progress.
  1. Download and install OCaml.
  2. Download our installation of CIL, which includes the cXprop source.
  3. Untar the tarball where you want it to live.
  4. Go into the cXprop-cil directory.
  5. Run ./configure --target=ARCH, where ARCH is either native (for your desktop), avr (for the atmega128), msp (for the msp430), or 8051 (for the 8051).
  6. Run make.
  7. Make sure the CIL's bin directory (cXprop-cil/bin) is in your path.
  8. Go to it. The script cXprop in the cXprop/bin directory runs CIL with the cXprop options most commonly used for desktop compilation. The cXpropMICA2 and cXpropTELOSB incorporate commonly used options for the mica2 and telosb mote platforms.

Top

Use

If you just run "cilly" it will give you a long list of command options. Most of those do not normally apply, but you should see a group of them clumped together which have "cxp" somewhere in their name. Those are the ones pertaining to conditional X propagation.

There are some useful CIL flags when running the analysis. Most notably is --save-temps, which causes the C code generated by CIL to be saved instead of discarded. This is useful for looking at the results of the analysis. It is also essential when compiling TinyOS applications, as you then must feed this saved source into avr-gcc. Another useful flag is --merge. This option causes all the C passed to cilly to be merged together and analyzed as a whole instead of each one individually.

Of course, the point of cXprop is to have multiple domains. Right now, our domain interface is cool, but the method of plugging things into that interface is a little clunky. To change domains, run the create_links.pl script in the src/ext/cxp directory. This script can also be used to change the platform assumed for machine dependencies, but the preferred method is now to rerun configure with the desired platform.

You can run cXprop on fcn_return.c and then look at the results by executing the following commands:

cXprop --save-temps fcn_return.c ; emacs fcn_return.cil.c

Included in this distribution is Will Archer's inliner. It can be run by adding a couple of options to the cXprop command. The basic options look like this are --doinliner --inline-auto, but others exist.

Please email me with any questions or comments or feedback! I am eager to help.

Top

Publications and Presentations

Static Analysis of Embedded C. John Regehr and Nathan Cooprider. St. Louis, Missouri. January 2008.
Static Analysis of Embedded C Code. John Regehr and Nathan Cooprider. Sydney, Australia. November 2007.
Pluggable Domains for C Dataflow Analysis. Nathan Cooprider and John Regehr. School of Computing, Utah. January 2007.
Pluggable Abstract Domains for Analyzing Embedded Software. Nathan Cooprider and John Regehr. In Proceedings of the ACM Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), Ottawa, Canada, June 2006.
cXprop: Postpass optimization for TinyOS applications. Nathan Cooprider and John Regehr. Poster for University of Utah School of Computing Research Day, Salt Lake City, Utah, March 2006.
cXprop: Postpass optimization for TinyOS applications. Nathan Cooprider and John Regehr. Poster in TinyOS Technology Exchange (TTX), Stanford, California, February 2006.
cXprop: Pluggable Domains for C Dataflow Analysis. Nathan Cooprider and John Regehr. Presentation in Program Analysis Seminar (CS 7938), Salt Lake City, Utah, September 2005.
A Static Analysis Framework for Embedded Systems. Nathan Cooprider and John Regehr. Presentation in Utah Regional Verification Workshop (URVW), Provo, Utah, May 2005.
Static Analysis for Embedded Systems. Nathan Cooprider. Poster in University of Utah School of Computing Research Day, Salt Lake City, Utah, April 2005.

Top

Links

Top

cXprop logo done by Jim Cooprider - jim34 AT cox DOT net

Back