Skip to content

Commit

Permalink
New command-line option for the RNG seed
Browse files Browse the repository at this point in the history
The pRNG seed can be set from the command-line using the --vr-seed
command-line switch:

  valgrind --tool=verrou --rounding-mode=random --vr-seed=12345
  • Loading branch information
ffevotte committed Jun 12, 2017
1 parent 6cc83c0 commit 7d0c871
Show file tree
Hide file tree
Showing 3 changed files with 11 additions and 15 deletions.
8 changes: 8 additions & 0 deletions vr_clo.c
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@
*/

#include "vr_main.h"
#include "vr_rand.h"

void vr_env_clo (const HChar* env, const HChar *clo) {
HChar* val = VG_(getenv)(env);
Expand Down Expand Up @@ -59,6 +60,8 @@ void vr_clo_defaults (void) {
for(opIt=0 ; opIt<VR_OP ; opIt++){
vr.instr_op[opIt]=False;
}

vr_rand_autoSeed (&vr_rand);
}

Bool vr_process_clo (const HChar *arg) {
Expand Down Expand Up @@ -136,6 +139,11 @@ Bool vr_process_clo (const HChar *arg) {
vr.includeSource = vr_loadIncludeSourceList(vr.includeSource, str);
}

// Set the pseudo-Random Number Generator
else if (VG_STR_CLO (arg, "--vr-seed", str)) {
vr_rand_setSeed (&vr_rand, VG_(strtoull10)(str, NULL));
}

// Unknown option
else{
return False;
Expand Down
17 changes: 3 additions & 14 deletions vr_fpOps.cxx
Original file line number Diff line number Diff line change
Expand Up @@ -30,26 +30,15 @@
The GNU General Public License is contained in the file COPYING.
*/

#include <cstdlib>
#include <ctime>
//#include <iostream>
//#include <cmath>
#include "math.h"
#include "pub_tool_libcfile.h"
#include "vr_fpRepr.hxx"
#include "vr_fpOps.h"
#include "vr_fma.h"

//#include "pub_tool_vki.h"

extern "C" {
#include <stdio.h>
#include "pub_tool_libcprint.h"
#include "vr_rand.h"
}

#include "pub_tool_basics.h"
#include "pub_tool_libcfile.h"

#include "vr_fpRepr.hxx"

// Forward declarations
template <typename REAL>
Expand Down Expand Up @@ -143,7 +132,7 @@ void vr_fpOpsInit (vr_RoundingMode mode) {

if (ROUNDINGMODE == VR_RANDOM
or ROUNDINGMODE == VR_AVERAGE) {
vr_rand_autoSeed (&vr_rand);
VG_(umsg)("First seed : %u\n", vr_rand_getSeed (&vr_rand));
}


Expand Down
1 change: 0 additions & 1 deletion vr_rand.c
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,6 @@ void vr_rand_autoSeed (Vr_Rand * r) {
unsigned int pid = VG_(getpid)();
unsigned int seed = now.tv_usec + pid;
vr_rand_setSeed (r, seed);
VG_(umsg)("First seed : %u\n", vr_rand_getSeed(r));
}

unsigned int vr_rand_getSeed (Vr_Rand * r) {
Expand Down

0 comments on commit 7d0c871

Please sign in to comment.