s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

dv.cc/iv.cc: When converting from an MTBDD, check that we don't write outside of the DoubleVector/IntegerVector 

The conversion functions expect that the MTBDD is non-zero only for the reachable states
(as seen by the ODD). If this is not the case due to programmer error, writes outside
the allocated vector can happen and will lead to hard to debug phenomena.

The protection does a hard exit when it detects this problem.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10549 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
d791bce62f
commit
f1aa7edc01
2 changed files with 27 additions and 19 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      prism/src/dv/dv.cc
  2. 16
      prism/src/dv/iv.cc

16
prism/src/dv/dv.cc
View File

@ -31,7 +31,7 @@
// local function prototypes
static void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, double *res);
static void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, long n, double *res);
static DdNode *double_vector_to_mtbdd_rec(DdManager *ddman, double *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, double value1, double value2, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, double d, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
@ -62,7 +62,7 @@ EXPORT double *mtbdd_to_double_vector(DdManager *ddman, DdNode *dd, DdNode **var
EXPORT double *mtbdd_to_double_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd, double *res)
{
int i, n;
long i, n;
// determine size
n = odd->eoff + odd->toff;
@ -73,18 +73,22 @@ EXPORT double *mtbdd_to_double_vector(DdManager *ddman, DdNode *dd, DdNode **var
res[i] = 0.0;
}
// build array recursively
mtbdd_to_double_vector_rec(ddman, dd, vars, num_vars, 0, odd, 0, res);
mtbdd_to_double_vector_rec(ddman, dd, vars, num_vars, 0, odd, 0, n, res);
return res;
}
void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, double *res)
void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, long n, double *res)
{
DdNode *e, *t;
if (dd == Cudd_ReadZero(ddman)) return;
if (level == num_vars) {
if (o < 0 || o >= n) {
printf("Internal error: Can not convert MTBDD to double vector: Value out of range of the ODD (does the MTBDD encode non-reachable states?)\n");
exit(1);
}
res[o] = Cudd_V(dd);
return;
}
@ -96,8 +100,8 @@ void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int
t = Cudd_T(dd);
}
mtbdd_to_double_vector_rec(ddman, e, vars, num_vars, level+1, odd->e, o, res);
mtbdd_to_double_vector_rec(ddman, t, vars, num_vars, level+1, odd->t, o+odd->eoff, res);
mtbdd_to_double_vector_rec(ddman, e, vars, num_vars, level+1, odd->e, o, n, res);
mtbdd_to_double_vector_rec(ddman, t, vars, num_vars, level+1, odd->t, o+odd->eoff, n, res);
}
//------------------------------------------------------------------------------

16
prism/src/dv/iv.cc
View File

@ -31,7 +31,7 @@
// local function prototypes
static void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, int *res);
static void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, long n, int *res);
static DdNode *integer_vector_to_mtbdd_rec(DdManager *ddman, int *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
//------------------------------------------------------------------------------
@ -51,7 +51,7 @@ EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars,
EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd, int *res)
{
int i, n;
long i, n;
// determine size
n = odd->eoff + odd->toff;
@ -62,18 +62,22 @@ EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars,
res[i] = 0.0;
}
// build array recursively
mtbdd_to_integer_vector_rec(ddman, dd, vars, num_vars, 0, odd, 0, res);
mtbdd_to_integer_vector_rec(ddman, dd, vars, num_vars, 0, odd, 0, n, res);
return res;
}
void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, int *res)
void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, long n, int *res)
{
DdNode *e, *t;
if (dd == Cudd_ReadZero(ddman)) return;
if (level == num_vars) {
if (o < 0 || o >= n) {
printf("Internal error: Can not convert MTBDD to integer vector: Value out of range of the ODD (does the MTBDD encode non-reachable states?)\n");
exit(1);
}
res[o] = (int) Cudd_V(dd);
return;
}
@ -85,8 +89,8 @@ void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, in
t = Cudd_T(dd);
}
mtbdd_to_integer_vector_rec(ddman, e, vars, num_vars, level+1, odd->e, o, res);
mtbdd_to_integer_vector_rec(ddman, t, vars, num_vars, level+1, odd->t, o+odd->eoff, res);
mtbdd_to_integer_vector_rec(ddman, e, vars, num_vars, level+1, odd->e, o, n, res);
mtbdd_to_integer_vector_rec(ddman, t, vars, num_vars, level+1, odd->t, o+odd->eoff, n, res);
}
//------------------------------------------------------------------------------

Write Preview
Loading…
Cancel
Save