andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Removed debugging stuff, now that the memory stuff is solved. It

Browse Source 
turned out that I solved the memory leak first, and then spent an
  afternoon finding the 8 blocks. These were simply not being given back
  by memrealloc, which I should have guessed.
This commit is contained in:
ccremers 2004-12-09 13:34:36 +00:00
parent c7d9517eac
commit 4f36181c3c
2 changed files with 13 additions and 66 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

65
src/arachne.c
View File

@ -667,20 +667,16 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
int flag; int flag;
int newgoals; int newgoals;
findLoserBegin (graph_uordblks);
run = semiRunCreate (p, r); run = semiRunCreate (p, r);
proof_suppose_run (run, 0, index + 1); proof_suppose_run (run, 0, index + 1);
{ {
findLoserBegin (graph_uordblks);
newgoals = add_read_goals (run, 0, index + 1); newgoals = add_read_goals (run, 0, index + 1);
indentDepth++; indentDepth++;
flag = bind_existing_to_goal (b, run, index); flag = bind_existing_to_goal (b, run, index);
indentDepth--; indentDepth--;
goal_remove_last (newgoals); goal_remove_last (newgoals);
findLoserEnd (graph_uordblks, "bind_new_run: add read goals");
} }
semiRunDestroy (); semiRunDestroy ();
findLoserEnd (graph_uordblks, "bind_new_run: inner");
return flag; return flag;
} }
@ -1290,7 +1286,6 @@ bind_goal_new_m0 (const Binding b)
int flag; int flag;
int found; int found;
findLoserBegin(graph_uordblks);
flag = 1; flag = 1;
found = 0; found = 0;
@ -1300,7 +1295,6 @@ bind_goal_new_m0 (const Binding b)
{ {
Term m0t; Term m0t;
Termlist subst; Termlist subst;
findLoserBegin (graph_uordblks);
m0t = tl->term; m0t = tl->term;
subst = termMguTerm (b->term, m0t); subst = termMguTerm (b->term, m0t);
@ -1308,13 +1302,11 @@ bind_goal_new_m0 (const Binding b)
{ {
int run; int run;
findLoserBegin (graph_uordblks);
I_M->roledef->message = m0t; I_M->roledef->message = m0t;
run = semiRunCreate (INTRUDER, I_M); run = semiRunCreate (INTRUDER, I_M);
proof_suppose_run (run, 0, 1); proof_suppose_run (run, 0, 1);
sys->runs[run].length = 1; sys->runs[run].length = 1;
{ {
findLoserBegin (graph_uordblks);
indentDepth++; indentDepth++;
if (goal_bind (b, run, 0)) if (goal_bind (b, run, 0))
{ {
@ -1335,18 +1327,15 @@ bind_goal_new_m0 (const Binding b)
} }
goal_unbind (b); goal_unbind (b);
indentDepth--; indentDepth--;
findLoserEnd (graph_uordblks, "bind goal new m0 sugar core");
} }
semiRunDestroy (); semiRunDestroy ();
findLoserEnd (graph_uordblks, "bind goal new m0: inner loop 2");
termlistSubstReset (subst); termlistSubstReset (subst);
termlistDelete (subst); termlistDelete (subst);
} }
tl = tl->next; tl = tl->next;
findLoserEnd(graph_uordblks, "bind goal new m0: inner loop");
} }
if (found == 0 && sys->output == PROOF) if (found == 0 && sys->output == PROOF)
@ -1358,7 +1347,6 @@ bind_goal_new_m0 (const Binding b)
} }
termlistDelete (m0tl); termlistDelete (m0tl);
findLoserEnd(graph_uordblks, "bind goal new m0");
return flag; return flag;
} }
@ -1374,7 +1362,6 @@ bind_goal_new_encrypt (const Binding b)
int flag; int flag;
int can_be_encrypted; int can_be_encrypted;
findLoserBegin(graph_uordblks);
flag = 1; flag = 1;
term = deVar (b->term); term = deVar (b->term);
@ -1419,25 +1406,21 @@ bind_goal_new_encrypt (const Binding b)
termPrint (t2); termPrint (t2);
eprintf ("\n"); eprintf ("\n");
} }
{ // indenting purely added for findLoser newgoals = add_read_goals (run, 0, index + 1);
findLoserBegin(graph_uordblks);
newgoals = add_read_goals (run, 0, index + 1);
indentDepth++; indentDepth++;
if (goal_bind (b, run, index)) if (goal_bind (b, run, index))
{ {
proof_suppose_binding (b); proof_suppose_binding (b);
flag = flag && iterate (); flag = flag && iterate ();
}
else
{
proof_cannot_bind (b, run, index);
}
goal_unbind (b);
indentDepth--;
goal_remove_last (newgoals);
findLoserEnd(graph_uordblks, "Goal bindings within m0 new");
} }
else
{
proof_cannot_bind (b, run, index);
}
goal_unbind (b);
indentDepth--;
goal_remove_last (newgoals);
semiRunDestroy (); semiRunDestroy ();
} }
} }
@ -1453,7 +1436,6 @@ bind_goal_new_encrypt (const Binding b)
} }
} }
findLoserEnd(graph_uordblks, "bind goal new encrypt");
return flag; return flag;
} }
@ -1526,7 +1508,6 @@ bind_goal_regular_run (const Binding b)
NULL)) NULL))
{ {
int sflag; int sflag;
findLoserBegin (graph_uordblks);
// A good candidate // A good candidate
found++; found++;
@ -1554,12 +1535,9 @@ bind_goal_regular_run (const Binding b)
sflag = bind_existing_run (b, p, r, index); sflag = bind_existing_run (b, p, r, index);
// bind to new run // bind to new run
{ {
findLoserBegin (graph_uordblks);
sflag = sflag && bind_new_run (b, p, r, index); sflag = sflag && bind_new_run (b, p, r, index);
findLoserEnd (graph_uordblks, "bind this role send; new run");
} }
indentDepth--; indentDepth--;
findLoserEnd (graph_uordblks, "bind this role send x");
return sflag; return sflag;
} }
else else
@ -1670,19 +1648,15 @@ bind_goal (const Binding b)
proofDepth++; proofDepth++;
if (know_only) if (know_only)
{ {
findLoserBegin (graph_uordblks);
// Special case: only from intruder // Special case: only from intruder
flag = flag && bind_goal_old_intruder_run (b); flag = flag && bind_goal_old_intruder_run (b);
flag = flag && bind_goal_new_intruder_run (b); flag = flag && bind_goal_new_intruder_run (b);
findLoserEnd (graph_uordblks, "bind_goal intruder case");
} }
else else
{ {
// Normal case // Normal case
{ {
findLoserBegin (graph_uordblks);
flag = bind_goal_regular_run (b); flag = bind_goal_regular_run (b);
findLoserEnd (graph_uordblks, "bind_goal case regular run");
} }
flag = flag && bind_goal_old_intruder_run (b); flag = flag && bind_goal_old_intruder_run (b);
flag = flag && bind_goal_new_intruder_run (b); flag = flag && bind_goal_new_intruder_run (b);
@ -1817,18 +1791,15 @@ prune_theorems ()
// Check for c-minimality // Check for c-minimality
{ {
findLoserBegin(graph_uordblks);
if (!bindings_c_minimal ()) if (!bindings_c_minimal ())
{ {
if (sys->output == PROOF) if (sys->output == PROOF)
{ {
findLoserBegin(graph_uordblks);
indentPrint (); indentPrint ();
eprintf ("Pruned because this is not <=c-minimal.\n"); eprintf ("Pruned because this is not <=c-minimal.\n");
} }
return 1; return 1;
} }
findLoserEnd(graph_uordblks, "C-minimality test");
} }
/** /**
@ -2079,15 +2050,12 @@ iterate ()
{ {
int flag; int flag;
findLoserBegin(graph_uordblks);
flag = 1; flag = 1;
if (!prune_theorems ()) if (!prune_theorems ())
{ {
findLoserBegin(graph_uordblks);
if (!prune_claim_specifics ()) if (!prune_claim_specifics ())
{ {
findLoserBegin(graph_uordblks);
if (!prune_bounds ()) if (!prune_bounds ())
{ {
Binding b; Binding b;
@ -2123,9 +2091,7 @@ iterate ()
/* /*
* bind this goal in all possible ways and iterate * bind this goal in all possible ways and iterate
*/ */
findLoserBegin (graph_uordblks);
flag = bind_goal (b); flag = bind_goal (b);
findLoserEnd (graph_uordblks, "bind_goal outer");
} }
} }
else else
@ -2133,9 +2099,7 @@ iterate ()
// Pruned because of bound! // Pruned because of bound!
current_claim->complete = 0; current_claim->complete = 0;
} }
findLoserEnd(graph_uordblks, "just outside prune_bounds condition");
} }
findLoserEnd(graph_uordblks, "just outside prune_claim_specifics condition");
} }
#ifdef DEBUG #ifdef DEBUG
@ -2145,9 +2109,6 @@ iterate ()
} }
#endif #endif
#ifdef DEBUG
findLoserEnd (graph_uordblks, "iterate");
#endif
return flag; return flag;
} }

14
src/binding.c
View File

@ -97,7 +97,6 @@ bindingDone ()
void void
goal_graph_destroy () goal_graph_destroy ()
{ {
findLoserBegin (graph_uordblks);
if (graph != NULL) if (graph != NULL)
{ {
#ifdef DEBUG #ifdef DEBUG
@ -117,7 +116,6 @@ goal_graph_destroy ()
graph_uordblks = 0; graph_uordblks = 0;
nodes = 0; nodes = 0;
} }
findLoserEnd (graph_uordblks, "goal_graph_destroy");
} }
//! Compute unclosed graph //! Compute unclosed graph
@ -127,7 +125,6 @@ goal_graph_create ()
int run, ev; int run, ev;
int last_m; int last_m;
List bl; List bl;
findLoserBegin (graph_uordblks);
goal_graph_destroy (); goal_graph_destroy ();
@ -140,17 +137,14 @@ goal_graph_create ()
if (graph_uordblks != 0) if (graph_uordblks != 0)
error ("Trying to create graph stuff without 0 uordblks for it first, but it is %i.", graph_uordblks); error ("Trying to create graph stuff without 0 uordblks for it first, but it is %i.", graph_uordblks);
findLoserBegin (graph_uordblks);
create_mi = mallinfo(); create_mi = mallinfo();
create_mem_before = create_mi.uordblks; create_mem_before = create_mi.uordblks;
graph = memAlloc ((nodes * nodes) * sizeof (int)); graph = memAlloc ((nodes * nodes) * sizeof (int));
create_mi = mallinfo(); create_mi = mallinfo();
graph_uordblks = create_mi.uordblks - create_mem_before; graph_uordblks = create_mi.uordblks - create_mem_before;
findLoserEnd (graph_uordblks, "core graph creation??");
} }
{ {
findLoserBegin (graph_uordblks);
graph_fill (graph, nodes, 0); graph_fill (graph, nodes, 0);
@ -159,7 +153,6 @@ goal_graph_create ()
last_m = -1; // last I_M run last_m = -1; // last I_M run
while (run < sys->maxruns) while (run < sys->maxruns)
{ {
findLoserBegin (graph_uordblks);
ev = 1; ev = 1;
//!@todo This now reference to step, but we intend "length" as in Arachne. //!@todo This now reference to step, but we intend "length" as in Arachne.
while (ev < sys->runs[run].step) while (ev < sys->runs[run].step)
@ -178,13 +171,11 @@ goal_graph_create ()
} }
// Next // Next
run++; run++;
findLoserEnd (graph_uordblks, "goal_graph_create: runloop");
} }
// Setup bindings order // Setup bindings order
bl = sys->bindings; bl = sys->bindings;
while (bl != NULL) while (bl != NULL)
{ {
findLoserBegin (graph_uordblks);
Binding b; Binding b;
b = (Binding) bl->data; b = (Binding) bl->data;
@ -201,13 +192,11 @@ goal_graph_create ()
(nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] = 1; (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] = 1;
} }
bl = bl->next; bl = bl->next;
findLoserEnd (graph_uordblks, "goal_graph_create: bindings loop");
} }
// Setup local constants order // Setup local constants order
run = 0; run = 0;
while (run < sys->maxruns) while (run < sys->maxruns)
{ {
findLoserBegin (graph_uordblks);
if (sys->runs[run].protocol != INTRUDER) if (sys->runs[run].protocol != INTRUDER)
{ {
int run2; int run2;
@ -345,11 +334,8 @@ goal_graph_create ()
} }
} }
run++; run++;
findLoserEnd (graph_uordblks, "goal_graph_create local constants loop");
} }
findLoserEnd (graph_uordblks, "goal_graph_create: constructing graph innards");
} }
findLoserEnd (graph_uordblks, "goal_graph_create");
} }