Commit dcf2bffd authored by johnvg@science.ru.nl's avatar johnvg@science.ru.nl
Browse files

in the strictness analyser, add code for caching previous results of LtExp2 to...

in the strictness analyser, add code for caching previous results of LtExp2 to prevent exponential time, not yet enabled
parent 5762c259
......@@ -849,6 +849,10 @@ static Exp *s_exp1, *s_exp2, *q_exp;
static long lt_exp2_max_n_calls;
/* */
/* LtExp2 may take exponential time if expressions are shared,
if CACHE_LT_EXP is defined extra code prevents this in most cases
by storing previous results using e_lt_cached, e_fwd and e_lt_result */
static Bool LtExp2 (Exp e1, Exp e2)
{
unsigned n, i;
......@@ -866,7 +870,10 @@ static Bool LtExp2 (Exp e1, Exp e2)
#endif
if (e1 == e2)
return True;
#ifdef CACHE_LT_EXP
if (e1->e_lt_cached && e1->e_fwd==e2)
return e1->e_lt_result;
#endif
if (e1->e_mark || e2->e_mark)
return MightBeTrue;
......@@ -892,6 +899,11 @@ static Bool LtExp2 (Exp e1, Exp e2)
e1->e_mark = True;
if (LtExp2 (e1->e_args[0], e2)){
e1->e_mark = False;
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = True;
#endif
return True;
}
e1->e_mark = False;
......@@ -928,6 +940,11 @@ static Bool LtExp2 (Exp e1, Exp e2)
case MightBeTrue:
e1->e_mark = False;
e2->e_mark = False;
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = MightBeTrue;
#endif
return MightBeTrue;
case False:
case AreRelated:
......@@ -937,6 +954,11 @@ static Bool LtExp2 (Exp e1, Exp e2)
} else {
e1->e_mark = False;
e2->e_mark = False;
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = False;
#endif
return False;
}
}
......@@ -946,9 +968,20 @@ static Bool LtExp2 (Exp e1, Exp e2)
if (s_index >= 0){
s_exp1 = & e1->e_args[s_index];
s_exp2 = & e2->e_args[s_index];
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = AreRelated;
#endif
return AreRelated;
} else
} else {
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = True;
#endif
return True;
}
}
case Lub:
e1->e_mark = True;
......@@ -959,10 +992,20 @@ static Bool LtExp2 (Exp e1, Exp e2)
b = LtExp2 (e1->e_args[i], e2);
if (b != True){
e1->e_mark = False;
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = b;
#endif
return b;
}
}
e1->e_mark = False;
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = True;
#endif
return True;
default:
Assume (False, "illegal case", "LtExp");
......@@ -983,25 +1026,80 @@ static Bool LtExp2 (Exp e1, Exp e2)
b = LtExp2 (e1, e2->e_args[i]);
if (b == True){
e2->e_mark = False;
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = b;
#endif
return b;
} else if (b == MightBeTrue)
result = MightBeTrue;
}
e2->e_mark = False;
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = result;
#endif
return result;
} else if (e2->e_kind == Ind){
e2->e_mark = True;
if (LtExp2 (e1, e2->e_args[0])){
e2->e_mark = False;
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = True;
#endif
return True;
}
e2->e_mark = False;
}
#ifdef CACHE_LT_EXP
e1->e_lt_cached = True;
e1->e_fwd = e2;
e1->e_lt_result = False;
#endif
return False;
}
#ifdef CACHE_LT_EXP
static void remove_lt_cached (Exp e)
{
unsigned n,i;
if (! e->e_lt_cached)
return;
e->e_lt_cached = False;
switch (e->e_kind){
case Top:
case Bottom:
case FunValue:
return;
case Ind:
remove_lt_cached (e->e_args[0]);
return;
case Argument:
return;
case Value:
n = e->e_fun->fun_arity;
break;
case Dep:
case Lub:
n = e->e_sym;
break;
default:
Assume (False, "unknown case", "remove_lt_cached");
return;
}
for (i = 0; i < n; i++)
remove_lt_cached (e->e_args[i]);
}
#endif
#ifdef _DB_
#undef Bool
Bool IsInAPath (Exp e1, Exp e2, APath p)
......@@ -1362,6 +1460,10 @@ static Bool LtExp (Exp e1, Exp e2)
/* */
b = LtExp2 (e1, e2);
#ifdef CACHE_LT_EXP
remove_lt_cached (e1);
#endif
#ifdef _DB_EQ_
if (DBPrinting){
if (b == True)
......
......@@ -31,19 +31,31 @@ typedef struct _dependency {
typedef Exp *ExpP;
#undef CACHE_LT_EXP
typedef struct _exp {
union {
unsigned short u_sym;
struct _fun * u_fun; /* if a value, a function id */
} e_u;
ExpKind e_kind; /* the kind of expression */
unsigned char e_hnf:1, /* set if reduced to hnf */
#ifdef CACHE_LT_EXP
unsigned short
#else
unsigned char
#endif
e_hnf:1, /* set if reduced to hnf */
e_spechnf:1, /* set if reduced in spec context */
e_hasind:1, /* used for indirections */
e_red:1, /* used for reductions */
e_imark:1, /* for marking use with Inds */
e_mark:1, /* for general use */
e_mark2:1; /* not for general use */
e_mark2:1 /* not for general use */
#ifdef CACHE_LT_EXP
,e_lt_cached:1,
e_lt_result:2
#endif
;
Exp *e_args; /* the arguments of the exp */
Exp e_fwd; /* for forwarding pointers */
Dependency e_deps; /* the current dependency list */
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment