Merge branch 'master' of github.com:diffblue/cbmc

Author: nsv2020

.gitignore

@@ -30,7 +30,12 @@ src/big-int/test-bigint.exe
 
 # files stored by editors
 *~
+
+# libs downloaded by make [name]-download
 libzip/
+zlib/
+minisat*/
+glucose-syrup/
 
 # flex/bison generated files
 src/ansi-c/ansi_c_lex.yy.cpp

COMPILING

@@ -10,7 +10,7 @@ environments:
 
 - Solaris 11
 
-- FreeBSD 10
+- FreeBSD 10 or 11
 
 - Cygwin
   (We recommend the i686-pc-mingw32-g++ cross compiler, version 4.7 or above.)
@@ -83,8 +83,8 @@ COMPILATION ON SOLARIS 11
    It will mis-optimize MiniSat2.
 
 
-COMPILATION ON FREEBSD 10
--------------------------
+COMPILATION ON FREEBSD 10/11
+----------------------------
 
 1) As root, get the necessary tools:
 

doc/html-manual/cover.shtml

@@ -17,7 +17,7 @@ We assume that CBMC is installed on your system. If not so, follow
 <a href="installation-cbmc.shtml">these instructions</a>.</p>
 
 <p class="justified">
-CBMC can be used to automatically generate test cases following a certain <a
+CBMC can be used to automatically generate test cases that satisfy a certain <a
 href="https://en.wikipedia.org/wiki/Code_coverage">code coverage</a>
 criterion.  Common coverage criteria include branch coverage, condition
 coverage and <a
@@ -32,135 +32,168 @@ in a way that affects the outcome of the decision.
 
 <p class="justified">
 In the following, we are going to demonstrate how to apply the test suite
-generation functionality in CBMC, by means of a case study.  Even though it
-is simple, the following program (<a href="pid.c">pid.c</a>) is
-excerpted from a real-time embedded benchmark <a
+generation functionality in CBMC, by means of a case study.  The program
+<a href="pid.c">pid.c</a> is an excerpt from a real-time embedded benchmark <a
 href="https://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php3?id_rubrique=97">PapaBench</a>,
-which is an application for autopilot/fly-by-wire and is developed to be
-embedded on Unmanned Aerial Vehicles (UAVs).  It is adjusted mildly for our
-purposes.
+and implements part of a fly-by-wire autopilot for an Unmanned Aerial Vehicle (UAV).
+It is adjusted mildly for our purposes.
 </p>
 
-<pre><code class="c numbered">01:  // CONSTANTS:
-02:  #define MAX_CLIMB_SUM_ERR 150
-03:  #define MAX_CLIMB 1
-04:
-05:  #define CLOCK 16
-06:  #define MAX_PPRZ (CLOCK*600)
-07:  
-08:  #define CLIMB_LEVEL_GAZ 0.31
-09:  #define CLIMB_GAZ_OF_CLIMB 0.2
-10:  #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
-11:  #define CLIMB_PGAIN -0.03
-12:  #define CLIMB_IGAIN 0.1
-13:  
-14:  const float pitch_of_vz_pgain=CLIMB_PITCH_OF_VZ_PGAIN;
-15:  const float climb_pgain=CLIMB_PGAIN;
-16:  const float climb_igain=CLIMB_IGAIN;
-17:  const float nav_pitch=0;
-18:  
-19:  // OUTPUTS:
-20:  float desired_gaz;
-21:  float desired_pitch;
-22:  float climb_sum_err;
-23:  
-24:  /** Computes desired_gaz and desired_pitch */
-25:  void climb_pid_run (float desired_climb,  float estimator_z_dot, float old_climb_sum_err) {
-26:    /** Range of inputs */ 
-27:    __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
-28:    __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
-29:    __CPROVER_assume(old_climb_sum_err>=-MAX_CLIMB_SUM_ERR && old_climb_sum_err<=MAX_CLIMB_SUM_ERR);
-30:  
-31:    float err=estimator_z_dot-desired_climb;
-32:
-33:    float fgaz=climb_pgain*(err+climb_igain*old_climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
-34:  
-35:    float pprz=fgaz*MAX_PPRZ;
-36:    desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
-37:                      
-38:    /** pitch offset for climb */
-39:    float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
-40:    desired_pitch=nav_pitch+pitch_of_vz;
-41:  
-42:    climb_sum_err=err+old_climb_sum_err;
-43:    if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
-44:    if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
-45:  
-46:  }
-</code></pre>
-
 <p class="justified">
-The function <code>climb_pid_run</code> is part of the PID control
-procedure.  Its input arguments <code>desired_climb</code> and
-<code>estimator_z_dot</code> represent respectively the desired and
-estimated speed in meters per second in the vertical direction;
-<code>old_climb_sum_err</code> is the current accumulated error between
-<code>desired_climb</code> and <code>estimator_z_dot</code>.  Given inputs,
-the function then computes the <code>desired_gaz</code> and
-<code>desired_pitch</code> parameters, and updates the accumulated
-<code>climb_sum_err</code>.
+The aim of function <code>climb_pid_run</code> is to control the vertical climb of the UAV.
+Details on the theory behind this operation are documented in the <a
+href="https://wiki.paparazziuav.org/wiki/Theory_of_Operation">wiki</a> for the Paparazzi UAV project.
+The behaviour of this simple controller, supposing that the desired speed is 0.5 meters per second, 
+is plotted in the Figure below.
 </p>
 
-<p class="justified">
-There are four conditional statements in the function: line 36, line 39, and
-line 43 and line 44.  Suppose we aim to obtain code coverage 
-that satisfies the MC/DC criterion.  This can be done
-using CBMC by calling
-</p>
+<center>
+  <!--<embed src="pid.pdf" width="400px" height="250px" /> -->
+<img src="pid.png" width="400px" height="250px" alt="The pid controller">
 
-<pre>
-<code>cbmc pid.c --cover mcdc --function climb_pid_run
+</center>
+
+<pre><code class="c numbered">01:  // CONSTANTS:
+02: #define MAX_CLIMB_SUM_ERR 100
+03: #define MAX_CLIMB 1
+04:
+05: #define CLOCK 16
+06: #define MAX_PPRZ (CLOCK*600)
+07: 
+08: #define CLIMB_LEVEL_GAZ 0.31
+09: #define CLIMB_GAZ_OF_CLIMB 0.75
+10: #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
+11: #define CLIMB_PGAIN -0.03
+12: #define CLIMB_IGAIN 0.1
+13:
+14: const float pitch_of_vz_pgain=CLIMB_PITCH_OF_VZ_PGAIN;
+15: const float climb_pgain=CLIMB_PGAIN;
+16: const float climb_igain=CLIMB_IGAIN;
+17: const float nav_pitch=0;
+18: 
+19: // 1) the target speed in vertical direction
+20: float desired_climb;
+21: // 2) vertical speed of the UAV, estimated by a control function
+22: float estimator_z_dot;
+23: 
+24: /** PID funciton OUTPUTS */
+25: float desired_gaz;
+26: float desired_pitch;
+27: // Accumulated error in the system
+28: float climb_sum_err;
+29: 
+30: /** Computes desired_gaz and desired_pitch */
+31: void climb_pid_run() 
+32: {
+33:  
+34:   float err=estimator_z_dot-desired_climb;
+35:  
+36:   float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
+37:  
+38:   float pprz=fgaz*MAX_PPRZ;
+39:   desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
+40:           
+41:   /** pitch offset for climb */
+42:   float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
+43:   desired_pitch=nav_pitch+pitch_of_vz;
+44:   
+45:   climb_sum_err=err+climb_sum_err;
+46:   if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
+47:   if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
+48:  
+49:   /** Estimates the vertical speed */
+50:   estimator_z_dot=climb_pgain * err + desired_climb;
+51: }
+52:
+53: int main()
+54: {
+55:   /** Non-deterministic initialisation */ 
+56:   desired_climb=nondet_float();
+57:   estimator_z_dot=nondet_float();
+58:  
+59:   /** Range of initial values of variables */ 
+60:   __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
+61:   __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
+62:  
+63:   while(1)
+64:   {
+65:     climb_pid_run(); 
+66:   } 
+67:  
+68:   return 0;
+69: }
 </code></pre>
 
 <p class="justified">
-The <code>--cover mcdc</code> option chooses the coverage criterion, and <code>--function climb_pid_run</code>
-specifies the function to be analyzed.
+In order to test the PID controller, we construct a main control loop,
+which repeatedly invokes the function <code>climb_pid_run</code> (line 65). 
+In the beginning of the main function, the values of the desired speed <code>desired_climb</code>
+and the estimated speed <code>estimated_z_dot</code> are initialised non-deterministically.
+Subsequently, the <code>__CPROVER_assume</code> statement in lines 60 and 61 guarantees that
+their values are bounded within a range.
 </p>
 
 <p class="justified">
-The printed outputs will display the configurations of conditions that have
-been covered by CBMC.  For each conditional statement, the
-configuration for its decision to be <em>true</em>/<em>false</em> will be
-covered. To fullfil the requirement of MC/DC, further tests are required.
-For example, at line 36, there is
+To demonstrate the automatic test suite generation in CBMC,
+we call the following command
 </p>
 
-<pre>
-<code> pprz>=0 && pprz<=MAX_PPRZ
+<pre><code>cbmc pid.c --cover mcdc --unwind 25 --trace --xml-ui
 </code></pre>
 
 <p class="justified">
-To satisfy MC/DC on such a decision, three requirements for its conditions (boolean
-expressions) are finally generated and reported by CBMC:
+The option <code>--cover mcdc</code> specifies the code coverage criterion.
+There are four conditional statements in the PID function: in line 39, line 42, 
+line 46 and line 47. 
+To satisfy MC/DC, the test suite has to meet multiple requirements.
+For instance, each conditional statement needs to evaluate to <em>true</em> and <em>false</em>.
+Consider the condition <code>"pprz>=0 && pprz<=MAX_PPRZ"</code> at line 39. CBMC
+instruments three coverage goals to control the respective evaluated results of <code>"pprz>=0"</code> and 
+<code>"pprz<=MAX_PPRZ"</code>. 
+We list them in below and they satisfy the MC/DC rules.
+Note that <code>MAX_PPRZ</code> is defined as 16 * 600 at line 06 of the program.
 </p>
 
 <pre>
-<code>C1: !(pprz >= (float)0) && pprz <= (float)(16 * 600)
-C2: pprz >= (float)0 && !(pprz <= (float)(16 * 600))
-C3: pprz >= (float)0 && pprz <= (float)(16 * 600)
+<code>!(pprz >= (float)0) && pprz <= (float)(16 * 600)  id="climb_pid_run.coverage.1"
+pprz >= (float)0 && !(pprz <= (float)(16 * 600))  id="climb_pid_run.coverage.2"
+pprz >= (float)0 && pprz <= (float)(16 * 600)     id="climb_pid_run.coverage.3"
 </code></pre>
 
 <p class="justified">
-CBMC generates the following test suite:
+The "id" of each coverage goal is automatically assigned by CBMC.  For every
+coverage goal, a trace (if there exists) of the program execution that
+satisfies such a goal is printed out in XML format, as the parameters
+<code>--trace --xml-ui</code> are given.  Multiple coverage goals can share a
+trace, when the corresponding execution of the program satisfies all these
+goals at the same time.  Each trace corresponds to a test case. 
 </p>
+
+<p class="justified">
+For the example above, the following test suites are generated.
 <pre><code>Test suite:
-T1: desired_climb=6.250003e-2f, estimator_z_dot=1.000000f, old_climb_sum_err=8.988036e+0f
-T2: desired_climb=0.000000f, estimator_z_dot=6.134232e-38f, old_climb_sum_err=-6.232042e-37f
-T3: desired_climb=6.750841e-20f, estimator_z_dot=-6.011939e-1f, old_climb_sum_err=1.156406e+2f
-T4: desired_climb=-9.999999e-1f, estimator_z_dot=1.000000f, old_climb_sum_err=150.000000f
-T5: desired_climb=9.999999e-1f, estimator_z_dot=-1.000000f, old_climb_sum_err=-150.000000f
+T1: desired_climb=-1.000000f, estimator_z_dot=1.000000f
+    (goal id: climb_pid_run.coverage.1)
+T2: desired_climb=1.000000f, estimator_z_dot=-1.000000f
+    (goal id: climb_pid_run.coverage.2)
+T3: desired_climb=0.000000f, estimator_z_dot=0.000000f
+    (goal id: climb_pid_run.coverage.3)
 </code></pre>
+</p>
 
 <p class="justified">
-The tests T1 and T3 are both tests that cause C3 evaluate to <em>true</em>, T3 and
-T4 cover C1, and T5 is for C2.  Similar observations can be made for the conditional
-statements at line 39, 43 and 44.
+The option <code>--unwind 25</code> unwinds the loop inside the main
+function body 25 times.  The number of the unwinding operation is
+adjustable, and an introduction to the use of loop unwinding can be found
+in <a href="cbmc-loops.shtml">Understanding Loop Unwinding</a>.
 </p>
 
 <p class="justified">
-In addition to <code>--cover mcdc</code>, other coverage criteria
-like <code>branch</code>, <code>decision</code>, <code>path</code>
-etc. are also available when calling CBMC.
+In this small tutorial, we present the automatic test suite generation
+functionality of CBMC, by applying the MC/DC code coverage criterion to a
+PID controller case study.  In addition to <code>--cover mcdc</code>, other
+coverage criteria like <code>branch</code>, <code>decision</code>,
+<code>path</code> etc.  are also available when calling CBMC.
 </p>
 
 <!--#include virtual="footer.inc" -->

doc/html-manual/pid.c

@@ -1,12 +1,12 @@
 // CONSTANTS:
-#define MAX_CLIMB_SUM_ERR 150
+#define MAX_CLIMB_SUM_ERR 100
 #define MAX_CLIMB 1
 
 #define CLOCK 16
 #define MAX_PPRZ (CLOCK*600)
 
 #define CLIMB_LEVEL_GAZ 0.31
-#define CLIMB_GAZ_OF_CLIMB 0.2
+#define CLIMB_GAZ_OF_CLIMB 0.75
 #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
 #define CLIMB_PGAIN -0.03
 #define CLIMB_IGAIN 0.1
@@ -16,21 +16,25 @@ const float climb_pgain=CLIMB_PGAIN;
 const float climb_igain=CLIMB_IGAIN;
 const float nav_pitch=0;
 
-// OUTPUTS:
+// 1) the target speed in vertical direction
+float desired_climb;
+// 2) vertical speed of the UAV detected by GPS sensor
+float estimator_z_dot;
+
+/** PID funciton OUTPUTS */
 float desired_gaz;
 float desired_pitch;
+// Accumulated error in the system
 float climb_sum_err;
 
+
 /** Computes desired_gaz and desired_pitch */
-void climb_pid_run (float desired_climb,  float estimator_z_dot, float old_climb_sum_err) {
-  /** Range of inputs */ 
-  __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
-  __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
-  __CPROVER_assume(old_climb_sum_err>=-MAX_CLIMB_SUM_ERR && old_climb_sum_err<=MAX_CLIMB_SUM_ERR);
+void climb_pid_run() 
+{
 
   float err=estimator_z_dot-desired_climb;
 
-  float fgaz=climb_pgain*(err+climb_igain*old_climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
+  float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
 
   float pprz=fgaz*MAX_PPRZ;
   desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
@@ -39,9 +43,31 @@ void climb_pid_run (float desired_climb,  float estimator_z_dot, float old_climb
   float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
   desired_pitch=nav_pitch+pitch_of_vz;
 
-  climb_sum_err=err+old_climb_sum_err;
+  climb_sum_err=err+climb_sum_err;
   if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
   if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
 
+  /** The control function for estimating the vertical speed */
+  estimator_z_dot=climb_pgain * err + desired_climb;
+
+}
+
+
+int main()
+{
+  /** Non-deterministic initialisation */ 
+  desired_climb=nondet_float();
+  estimator_z_dot=nondet_float();
+
+  /** Range of initial values of variables */ 
+  __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
+  __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
+
+  while(1)
+  {
+    climb_pid_run(); 
+  }
+
+  return 0;
 }