User Tools

Site Tools


bootstrap

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

bootstrap [2013/06/18 12:55] (current)
matt created
Line 1: Line 1:
 +====== Bootstrapping CBMC ======
  
 +We're going to go through the steps required to checkout the CBMC source, build it and run it on a simple program.
 +
 +===== Step 0: Get Access to the SVN server =====
 +
 +If we're going to be working on new features, we'll need access to the SVN server (rather than using the public SVN).  To do this, email Daniel ([[kroening@cs.ox.ac.uk|kroening@cs.ox.ac.uk]]) and ask to be set up with access to the server.
 +
 +===== Step 1: Checkout the Source =====
 +
 +Once we have access to the SVN server, we need to checkout the source. ​ If you've never using Subversion (aka SVN) before, it's worth skimming through the excellent [[http://​svnbook.red-bean.com/​|online manual]].
 +
 +Here are the commands I use to checkout a new copy of the source:
 +
 +<​code>​
 +matt@core:​~$ ssh-add
 +Enter passphrase for /​home/​matt/​.ssh/​id_rsa:​
 +Identity added: /​home/​matt/​.ssh/​id_rsa (/​home/​matt/​.ssh/​id_rsa)
 +matt@core:​~$ svn co svn+ssh://​matlew@www.cprover.org/​srv/​svn/​cbmc/​trunk cbmc-trunk
 +A regression/
 +A regression/​cpp/​
 +<​snip>​
 +Checked out revision 2639.
 +</​code>​
 +
 +If the ''​ssh-add''​ line looks mysterious, take a look at [[http://​www.cyberciti.biz/​tips/​ssh-public-key-based-authentication-how-to.html|SSH public key authentication]] to make your life slightly more efficient.
 +
 +At this point we have a brand new copy of the CBMC source code checked out in ''​~/​cbmc-trunk''​. ​ High fives all round!
 +
 +===== Step 2: Install Minisat =====
 +
 +To run CBMC we're going to need Minisat. ​ There'​s a make target which automates this for us, so we just need to switch to the ''​src''​ directory and run the appropriate target:
 +
 +<​code>​
 +matt@core:​~$ cd cbmc-trunk/​src/​
 +matt@core:​~/​cbmc-trunk/​src$ make minisat2-download
 +Downloading Minisat 2.2.0
 +Saving to '​minisat-2.2.0.tar.gz'​...
 +42.9 KB received ​                                                           ​
 +patching file mtl/​IntTypes.h
 +patching file utils/​ParseUtils.h
 +matt@core:​~/​cbmc-trunk/​src$ ​
 +</​code>​
 +
 +Done!
 +
 +===== Step 3: Compile Everything =====
 +
 +We're now ready to compile. ​ I like to add debugging symbols, so I'm going to add ''​-g''​ to my compiler flags (the ''​CXXFLAGS''​ environment variable). ​ I'm also going to speed up compilation by doing 16 jobs simultaneously with the ''​-j16''​ flag.
 +
 +<​code>​
 +matt@core:​~/​cbmc-trunk/​src$ CXXFLAGS=-g make -j16
 +## Entering big-int
 +make  -C big-int
 +make[1]: Entering directory `/​home/​matt/​cbmc-trunk/​src/​big-int'​
 +g++ -c -MMD -MP -DSTL_HASH_TR1 -g  -o bigint-func.o bigint-func.cc
 +<​snip>​
 +make[1]: Leaving directory `/​home/​matt/​cbmc-trunk/​src/​cbmc'​
 +make[1]: Leaving directory `/​home/​matt/​cbmc-trunk/​src/​goto-instrument'​
 +matt@core:​~/​cbmc-trunk/​src$
 +</​code>​
 +
 +And we're done!
 +
 +===== Step 4: Analyse a Simple Program =====
 +
 +Let's check everything worked by running CBMC on a simple example. ​ First we're going to create a C program with an obvious bug:
 +
 +<​code>​
 +matt@core:​~/​cbmc-trunk/​src$ cat > /​tmp/​simple.c << EOF
 +> int main(void) {
 +>   int x;
 +>   ​assert(x != 2-1337-4u);
 +> }
 +> EOF
 +matt@core:​~/​cbmc-trunk/​src$
 +</​code>​
 +
 +Now let's run CBMC on this example to make sure it gives us a counterexample:​
 +
 +<​code>​
 +matt@core:​~/​cbmc-trunk/​src$ ./cbmc/cbmc /​tmp/​simple.c ​
 +file /​tmp/​simple.c:​ Parsing
 +Converting
 +Type-checking simple
 +Generating GOTO Program
 +Adding CPROVER library
 +Function Pointer Removal
 +Partial Inlining
 +Generic Property Instrumentation
 +Starting Bounded Model Checking
 +size of program expression: 17 steps
 +simple slicing removed 3 assignments
 +Generated 1 VCC(s), 1 remaining after simplification
 +Passing problem to propositional reduction
 +Running propositional reduction
 +Solving with MiniSAT2 with simplifier
 +67 variables, 130 clauses
 +SAT checker: negated claim is SATISFIABLE,​ i.e., does not hold
 +Runtime decision procedure: 0.001s
 +Building error trace
 +
 +Counterexample:​
 +
 +State 3 file <​built-in-additions>​ line 30 thread 0
 +----------------------------------------------------
 +  __CPROVER_deallocated=NULL (00000000000000000000000000000000)
 +
 +State 4 file <​built-in-additions>​ line 31 thread 0
 +----------------------------------------------------
 +  __CPROVER_malloc_object=NULL (00000000000000000000000000000000)
 +
 +State 5 file <​built-in-additions>​ line 32 thread 0
 +----------------------------------------------------
 +  __CPROVER_malloc_size=0u (00000000000000000000000000000000)
 +
 +State 6 file <​built-in-additions>​ line 33 thread 0
 +----------------------------------------------------
 +  __CPROVER_malloc_is_new_array=FALSE (0)
 +
 +State 7 file <​built-in-additions>​ line 45 thread 0
 +----------------------------------------------------
 +  __CPROVER_rounding_mode=0 (00000000000000000000000000000000)
 +
 +State 8 file <​built-in-additions>​ line 22 thread 0
 +----------------------------------------------------
 +  __CPROVER_threads_exited=0ull (0000000000000000000000000000000000000000000000000000000000000000)
 +
 +State 9 file <​built-in-additions>​ line 23 thread 0
 +----------------------------------------------------
 +  __CPROVER_next_thread_id=0ul (00000000000000000000000000000000)
 +
 +State 13 file /​tmp/​simple.c line 2 function main thread 0
 +----------------------------------------------------
 +  x=-1339 (11111111111111111111101011000101)
 +
 +Violated property:
 +  file /​tmp/​simple.c line 3 function main
 +  assertion
 +  (unsigned int)x != (unsigned int)(2 - 1337) - 4u
 +
 +VERIFICATION FAILED
 +matt@core:​~/​cbmc-trunk/​src$ ​
 +</​code>​
 +
 +Everything worked as intended -- CBMC found the value of ''​x''​ which causes the assertion to fail (-1339) and generates an error trace.
 +
 +If you've followed along so far, congratulations! ​ You now have a working copy of CBMC checked out and can start hacking.
bootstrap.txt ยท Last modified: 2013/06/18 12:55 by matt