Quickstart

In this quick tutorial, we will use Cloud9 to test a small C program that simulates a producer-consumer system. The system consists of a client process that produces a set of integer values, which are then sent to a consumer process. The producer instructs the consumer to terminate by sending a negative value at the end. The program makes use of the POSIX pthreads API, it forks processes, and does network communication, so we will use Cloud9's POSIX model to run it.

First, follow the instructions to setup Cloud9 on your machine. We assume you installed Cloud9 in $CLOUD9_ROOT.
Change the current directory to $CLOUD9_ROOT/src/testing_targets. This is where the code that gets compiled into LLVM bitcode reside.
Build all the LLVM bitcode:

$ build/gyp_testing_targets
$ build/make_all
You should find the prod-cons.bc LLVM binary in the out/Default directory. Let's now test it using Cloud9:

$ export GLOG_logtostderr=1
$ $CLOUD9_ROOT/src/cloud9/Release+Asserts/bin/c9-worker --stand-alone --posix-runtime --output-dir=test-prod-cons out/Default/prod-cons.bc

The first line configures the Cloud9 logging system to print the testing progress in the terminal, instead of writing it in a file under /tmp.
The second line spawns a Cloud9 worker that runs stand alone, and uses the POSIX environment model to support all the API calls performed by the producer-consumer code.

Cloud9 should complete execution within a few seconds, and output messages indicating the values that were produced/consumed, together with network state information (created sockets, initiated connections, etc.). The example program uses symbolic execution to a small extent. The producer marks as symbolic the last value to send to the consumer, and assumes that the value is negative, so the consumer would terminate.

That was quick, right? From this point, you can try testing other programs (memcached, Apache, Chromium's OpenType Sanitizer), and learn how to build LLVM binaries for your own testing targets.

Comments