zcov: / lib/Support/RNG.cpp


Files: 1 Branches Taken: 100.0% 8 / 8
Generated: 2009-05-17 22:47 Branches Executed: 100.0% 8 / 8
Line Coverage: 58.3% 28 / 48


Programs: 1 Runs 371


       1                 : /* 
       2                 :    A C-program for MT19937, with initialization improved 2002/1/26.
       3                 :    Coded by Takuji Nishimura and Makoto Matsumoto.
       4                 :    Modified to be a C++ class by Daniel Dunbar.
       5                 : 
       6                 :    Before using, initialize the state by using init_genrand(seed)  
       7                 :    or init_by_array(init_key, key_length).
       8                 : 
       9                 :    Copyright (C) 1997 - 2002, Makoto Matsumoto and Takuji Nishimura,
      10                 :    All rights reserved.                          
      11                 : 
      12                 :    Redistribution and use in source and binary forms, with or without
      13                 :    modification, are permitted provided that the following conditions
      14                 :    are met:
      15                 : 
      16                 :      1. Redistributions of source code must retain the above copyright
      17                 :         notice, this list of conditions and the following disclaimer.
      18                 : 
      19                 :      2. Redistributions in binary form must reproduce the above copyright
      20                 :         notice, this list of conditions and the following disclaimer in the
      21                 :         documentation and/or other materials provided with the distribution.
      22                 : 
      23                 :      3. The names of its contributors may not be used to endorse or promote 
      24                 :         products derived from this software without specific prior written 
      25                 :         permission.
      26                 : 
      27                 :    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
      28                 :    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
      29                 :    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
      30                 :    A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT OWNER OR
      31                 :    CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
      32                 :    EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
      33                 :    PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
      34                 :    PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
      35                 :    LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
      36                 :    NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
      37                 :    SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
      38                 : 
      39                 : 
      40                 :    Any feedback is very welcome.
      41                 :    http://www.math.sci.hiroshima-u.ac.jp/~m-mat/MT/emt.html
      42                 :    email: m-mat @ math.sci.hiroshima-u.ac.jp (remove space)
      43                 : */
      44                 : 
      45                 : #include "klee/Internal/ADT/RNG.h"
      46                 : 
      47                 : using namespace klee;
      48                 : 
      49                 : /* initializes mt[N] with a seed */
      50              103: RNG::RNG(unsigned int s) {
      51              103:   seed(s);
      52              103: }
      53                 : 
      54              103: void RNG::seed(unsigned int s) {
      55              103:   mt[0]= s & 0xffffffffUL;
                    64169: branch 0 taken
                      103: branch 1 taken
      56            64272:   for (mti=1; mti<N; mti++) {
      57                 :     mt[mti] = 
      58            64169:       (1812433253UL * (mt[mti-1] ^ (mt[mti-1] >> 30)) + mti); 
      59                 :     /* See Knuth TAOCP Vol2. 3rd Ed. P.106 for multiplier. */
      60                 :     /* In the previous versions, MSBs of the seed affect   */
      61                 :     /* only MSBs of the array mt[].                        */
      62                 :     /* 2002/01/09 modified by Makoto Matsumoto             */
      63            64169:     mt[mti] &= 0xffffffffUL;
      64                 :     /* for >32 bit machines */
      65                 :   }
      66              103: }
      67                 : 
      68                 : /* generates a random number on [0,0xffffffff]-interval */
      69             4252: unsigned int RNG::getInt32() {
      70                 :   unsigned int y;
      71                 :   static unsigned int mag01[2]={0x0UL, MATRIX_A};
      72                 :   /* mag01[x] = x * MATRIX_A  for x=0,1 */
      73                 :   
                       25: branch 0 taken
                     4227: branch 1 taken
      74             4252:   if (mti >= N) { /* generate N words at one time */
      75                 :     int kk;
      76                 :     
                     5675: branch 0 taken
                       25: branch 1 taken
      77             5700:     for (kk=0;kk<N-M;kk++) {
      78             5675:       y = (mt[kk]&UPPER_MASK)|(mt[kk+1]&LOWER_MASK);
      79             5675:       mt[kk] = mt[kk+M] ^ (y >> 1) ^ mag01[y & 0x1UL];
      80                 :     }
                     9900: branch 0 taken
                       25: branch 1 taken
      81             9900:     for (;kk<N-1;kk++) {
      82             9900:       y = (mt[kk]&UPPER_MASK)|(mt[kk+1]&LOWER_MASK);
      83             9900:       mt[kk] = mt[kk+(M-N)] ^ (y >> 1) ^ mag01[y & 0x1UL];
      84                 :     }
      85               25:     y = (mt[N-1]&UPPER_MASK)|(mt[0]&LOWER_MASK);
      86               25:     mt[N-1] = mt[M-1] ^ (y >> 1) ^ mag01[y & 0x1UL];
      87                 :     
      88               25:     mti = 0;
      89                 :   }
      90                 :   
      91             4252:   y = mt[mti++];
      92                 : 
      93                 :   /* Tempering */
      94             4252:   y ^= (y >> 11);
      95             4252:   y ^= (y << 7) & 0x9d2c5680UL;
      96             4252:   y ^= (y << 15) & 0xefc60000UL;
      97             4252:   y ^= (y >> 18);
      98                 :   
      99             4252:   return y;
     100                 : }
     101                 : 
     102                 : /* generates a random number on [0,0x7fffffff]-interval */
     103                0: int RNG::getInt31() {
     104                0:   return (int)(getInt32()>>1);
     105                 : }
     106                 : 
     107                 : /* generates a random number on [0,1]-real-interval */
     108                0: double RNG::getDoubleLR() {
     109                0:   return getInt32()*(1.0/4294967295.0); 
     110                 :   /* divided by 2^32-1 */ 
     111                 : }
     112                 : 
     113                 : /* generates a random number on [0,1)-real-interval */
     114             1112: double RNG::getDoubleL() {
     115             1112:   return getInt32()*(1.0/4294967296.0); 
     116                 :   /* divided by 2^32 */
     117                 : }
     118                 : 
     119                 : /* generates a random number on (0,1)-real-interval */
     120                0: double RNG::getDouble() {
     121                0:   return (((double)getInt32()) + 0.5)*(1.0/4294967296.0); 
     122                 :   /* divided by 2^32 */
     123                 : }
     124                 : 
     125                0: float RNG::getFloatLR() {
     126                0:   return getInt32()*(1.0f/4294967295.0f); 
     127                 :   /* divided by 2^32-1 */ 
     128                 : }
     129                0: float RNG::getFloatL() {
     130                0:   return getInt32()*(1.0f/4294967296.0f); 
     131                 :   /* divided by 2^32 */
     132                 : }
     133                0: float RNG::getFloat() {
     134                0:   return (getInt32() + 0.5f)*(1.0f/4294967296.0f); 
     135                 :   /* divided by 2^32 */
     136                 : }
     137                 : 
     138                0: bool RNG::getBool() {
     139                0:   unsigned bits = getInt32();
     140                0:   bits ^= bits >> 16;
     141                0:   bits ^= bits >> 8;
     142                0:   bits ^= bits >> 4;
     143                0:   bits ^= bits >> 2;
     144                0:   bits ^= bits >> 1;
     145                0:   return bits&1;
     146                 : }

Generated: 2009-05-17 22:47 by zcov