|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 .|
OverviewMany 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.
We are actively working on improving cXprop in the following four ways:
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
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.
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.
|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.|