- Fixed a memory error.
This commit is contained in:
ccremers
parent
35c55c9483
commit
f25f0abd4e
109
src/arachne.c
109
src/arachne.c
@ -111,7 +111,7 @@ arachneInit (const System mysys)
|
||||
add_event (READ, NULL);
|
||||
add_event (READ, NULL);
|
||||
add_event (SEND, NULL);
|
||||
I_RRS = add_role ("I_D: Encrypt");
|
||||
I_RRS = add_role ("I_E: Encrypt");
|
||||
|
||||
return;
|
||||
}
|
||||
@ -172,12 +172,12 @@ semiRunCreate (const Protocol p, const Role r)
|
||||
{
|
||||
int run;
|
||||
|
||||
run = sys->maxruns;
|
||||
if (p == INTRUDER)
|
||||
num_intruder_runs++;
|
||||
else
|
||||
num_regular_runs++;
|
||||
roleInstance (sys, p, r, NULL, NULL);
|
||||
run = sys->maxruns-1;
|
||||
sys->runs[run].length = 0;
|
||||
return run;
|
||||
}
|
||||
@ -186,14 +186,17 @@ semiRunCreate (const Protocol p, const Role r)
|
||||
void
|
||||
semiRunDestroy ()
|
||||
{
|
||||
Protocol p;
|
||||
if (sys->maxruns > 0)
|
||||
{
|
||||
Protocol p;
|
||||
|
||||
p = sys->runs[sys->maxruns - 1].protocol;
|
||||
roleInstanceDestroy (sys);
|
||||
if (p == INTRUDER)
|
||||
num_intruder_runs--;
|
||||
else
|
||||
num_regular_runs--;
|
||||
p = sys->runs[sys->maxruns - 1].protocol;
|
||||
roleInstanceDestroy (sys);
|
||||
if (p == INTRUDER)
|
||||
num_intruder_runs--;
|
||||
else
|
||||
num_regular_runs--;
|
||||
}
|
||||
}
|
||||
|
||||
//! After a role instance, or an extension of a run, we might need to add some goals
|
||||
@ -765,6 +768,7 @@ bind_goal_new_m0 (const Binding b)
|
||||
goal_unbind (b);
|
||||
indentDepth--;
|
||||
semiRunDestroy ();
|
||||
|
||||
termlistSubstReset (subst);
|
||||
termlistDelete (subst);
|
||||
}
|
||||
@ -792,9 +796,11 @@ bind_goal_new_encrypt (const Binding b)
|
||||
{
|
||||
Term term;
|
||||
int flag;
|
||||
int can_be_encrypted;
|
||||
|
||||
flag = 1;
|
||||
term = b->term;
|
||||
term = deVar(b->term);
|
||||
can_be_encrypted = 0;
|
||||
|
||||
if (!realTermLeaf (term))
|
||||
{
|
||||
@ -804,7 +810,7 @@ bind_goal_new_encrypt (const Binding b)
|
||||
Roledef rd;
|
||||
Term t1, t2;
|
||||
|
||||
if (realTermTuple (term))
|
||||
if (!realTermEncrypt (term))
|
||||
{
|
||||
// tuple construction
|
||||
error ("Goal that is a tuple should not occur!");
|
||||
@ -814,41 +820,47 @@ bind_goal_new_encrypt (const Binding b)
|
||||
t1 = term->left.op;
|
||||
t2 = term->right.key;
|
||||
|
||||
run = semiRunCreate (INTRUDER, I_RRS);
|
||||
rd = sys->runs[run].start;
|
||||
rd->message = termDuplicate (t1);
|
||||
rd->next->message = termDuplicate (t2);
|
||||
rd->next->next->message = termDuplicate (term);
|
||||
index = 2;
|
||||
proof_suppose_run (run, 0, index + 1);
|
||||
if (sys->output == PROOF)
|
||||
if (t2 != TERM_Hidden)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("* Encrypting ");
|
||||
termPrint (term);
|
||||
eprintf (" using term ");
|
||||
termPrint (t1);
|
||||
eprintf (" and key ");
|
||||
termPrint (t2);
|
||||
eprintf ("\n");
|
||||
can_be_encrypted = 1;
|
||||
run = semiRunCreate (INTRUDER, I_RRS);
|
||||
rd = sys->runs[run].start;
|
||||
//rd->message = termDuplicateUV (t1);
|
||||
//rd->next->message = termDuplicateUV (t2);
|
||||
rd->next->next->message = termDuplicateUV (term);
|
||||
index = 2;
|
||||
proof_suppose_run (run, 0, index + 1);
|
||||
if (sys->output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("* Encrypting ");
|
||||
termPrint (term);
|
||||
eprintf (" using term ");
|
||||
termPrint (t1);
|
||||
eprintf (" and key ");
|
||||
termPrint (t2);
|
||||
eprintf ("\n");
|
||||
}
|
||||
newgoals = add_read_goals (run, 0, index + 1);
|
||||
|
||||
indentDepth++;
|
||||
if (goal_bind (b, run, index))
|
||||
{
|
||||
proof_suppose_binding (b);
|
||||
flag = flag && iterate ();
|
||||
}
|
||||
else
|
||||
{
|
||||
proof_cannot_bind (b, run, index);
|
||||
}
|
||||
goal_unbind (b);
|
||||
indentDepth--;
|
||||
remove_read_goals (newgoals);
|
||||
semiRunDestroy ();
|
||||
}
|
||||
newgoals = add_read_goals (run, 0, index + 1);
|
||||
indentDepth++;
|
||||
if (goal_bind (b, run, index))
|
||||
{
|
||||
proof_suppose_binding (b);
|
||||
flag = flag && iterate ();
|
||||
}
|
||||
else
|
||||
{
|
||||
proof_cannot_bind (b, run, index);
|
||||
}
|
||||
goal_unbind (b);
|
||||
indentDepth--;
|
||||
remove_read_goals (newgoals);
|
||||
semiRunDestroy ();
|
||||
}
|
||||
else
|
||||
|
||||
if (!can_be_encrypted)
|
||||
{
|
||||
if (sys->output == PROOF)
|
||||
{
|
||||
@ -1375,26 +1387,25 @@ arachne ()
|
||||
proof_suppose_run (run, 0, cl->ev + 1);
|
||||
add_read_goals (run, 0, cl->ev + 1);
|
||||
|
||||
|
||||
/**
|
||||
* Add specific goal info
|
||||
*/
|
||||
add_claim_specifics (cl,
|
||||
roledef_shift (sys->runs[run].start, cl->ev));
|
||||
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
printSemiState ();
|
||||
}
|
||||
#endif
|
||||
|
||||
/*
|
||||
* iterate
|
||||
*/
|
||||
// Iterate
|
||||
iterate ();
|
||||
|
||||
//! Destroy
|
||||
while (sys->bindings != NULL)
|
||||
{
|
||||
remove_read_goals (1);
|
||||
}
|
||||
while (sys->maxruns > 0)
|
||||
{
|
||||
semiRunDestroy ();
|
||||
|
||||
126
src/term.c
126
src/term.c
@ -433,7 +433,7 @@ termDuplicate (const Term term)
|
||||
return term;
|
||||
|
||||
newterm = (Term) memAlloc (sizeof (struct term));
|
||||
newterm->type = term->type;
|
||||
memcpy (newterm, term, sizeof (struct term));
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
newterm->left.op = termDuplicate (term->left.op);
|
||||
@ -464,13 +464,9 @@ termDuplicateDeep (const Term term)
|
||||
return NULL;
|
||||
|
||||
newterm = (Term) memAlloc (sizeof (struct term));
|
||||
if (realTermLeaf (term))
|
||||
memcpy (newterm, term, sizeof (struct term));
|
||||
if (!realTermLeaf (term))
|
||||
{
|
||||
memcpy (newterm, term, sizeof (struct term));
|
||||
}
|
||||
else
|
||||
{
|
||||
newterm->type = term->type;
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
newterm->left.op = termDuplicateDeep (term->left.op);
|
||||
@ -496,14 +492,14 @@ termDuplicateUV (Term term)
|
||||
{
|
||||
Term newterm;
|
||||
|
||||
term = deVar (term);
|
||||
if (term == NULL)
|
||||
return NULL;
|
||||
term = deVar (term);
|
||||
if (realTermLeaf (term))
|
||||
return term;
|
||||
|
||||
newterm = (Term) memAlloc (sizeof (struct term));
|
||||
newterm->type = term->type;
|
||||
memcpy (newterm, term, sizeof (struct term));
|
||||
if (realTermEncrypt (term))
|
||||
{
|
||||
newterm->left.op = termDuplicateUV (term->left.op);
|
||||
@ -676,7 +672,7 @@ tupleCount (Term tt)
|
||||
}
|
||||
else
|
||||
{
|
||||
deVar (tt);
|
||||
tt = deVar (tt);
|
||||
if (!realTermTuple (tt))
|
||||
{
|
||||
return 1;
|
||||
@ -702,7 +698,7 @@ tupleProject (Term tt, int n)
|
||||
{
|
||||
return NULL;
|
||||
}
|
||||
deVar (tt);
|
||||
tt = deVar (tt);
|
||||
if (!realTermTuple (tt))
|
||||
{
|
||||
if (n > 0)
|
||||
@ -956,32 +952,62 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
|
||||
|
||||
if (noder != NULL)
|
||||
flag = flag && noder (term);
|
||||
|
||||
return flag;
|
||||
}
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
//! Generic term iteration with deVar
|
||||
//! Generic term iteration
|
||||
int
|
||||
term_iterate_deVar (const Term term, int (*leaf) (), int (*nodel) (),
|
||||
int (*nodem) (), int (*noder) ())
|
||||
term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
|
||||
int (*nodem) (), int (*noder) ())
|
||||
{
|
||||
int deVar_leaf (const Term term)
|
||||
{
|
||||
if (substVar (term))
|
||||
{
|
||||
return term_iterate_deVar (term->subst, deVar_leaf, nodel, nodem,
|
||||
noder);
|
||||
}
|
||||
else
|
||||
{
|
||||
if (leaf == NULL)
|
||||
return 1;
|
||||
else
|
||||
return leaf (term);
|
||||
}
|
||||
}
|
||||
return term_iterate (term, deVar_leaf, nodel, nodem, noder);
|
||||
term = deVar (term);
|
||||
if (term != NULL)
|
||||
{
|
||||
if (realTermLeaf (term))
|
||||
{
|
||||
// Leaf
|
||||
if (leaf != NULL)
|
||||
{
|
||||
return leaf (term);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
int flag;
|
||||
|
||||
flag = 1;
|
||||
|
||||
if (nodel != NULL)
|
||||
flag = flag && nodel (term);
|
||||
|
||||
if (realTermTuple (term))
|
||||
flag = flag
|
||||
&& (term_iterate_deVar (term->left.op1, leaf, nodel, nodem, noder));
|
||||
else
|
||||
flag = flag
|
||||
&& (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder));
|
||||
|
||||
if (nodem != NULL)
|
||||
flag = flag && nodem (term);
|
||||
|
||||
if (realTermTuple (term))
|
||||
flag = flag
|
||||
&& (term_iterate_deVar (term->left.op1, leaf, nodel, nodem, noder));
|
||||
else
|
||||
flag = flag
|
||||
&& (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder));
|
||||
|
||||
if (noder != NULL)
|
||||
flag = flag && noder (term);
|
||||
|
||||
return flag;
|
||||
}
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
//! Iterate over the leaves in a term
|
||||
@ -1082,26 +1108,36 @@ term_constrain_level (const Term term)
|
||||
int structure;
|
||||
int flag;
|
||||
|
||||
int leaf (const Term t)
|
||||
{
|
||||
structure++;
|
||||
if (realTermVariable (t))
|
||||
vars++;
|
||||
return 1;
|
||||
}
|
||||
int nodel (const Term t)
|
||||
{
|
||||
structure++;
|
||||
if (realTermTuple (t))
|
||||
structure++;
|
||||
return 1;
|
||||
}
|
||||
void
|
||||
tcl_iterate (Term t)
|
||||
{
|
||||
t = deVar (t);
|
||||
structure++;
|
||||
if (realTermLeaf (t))
|
||||
{
|
||||
if (realTermVariable (t))
|
||||
vars++;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (realTermTuple (t))
|
||||
{
|
||||
tcl_iterate (t->left.op1);
|
||||
tcl_iterate (t->right.op2);
|
||||
}
|
||||
else
|
||||
{
|
||||
tcl_iterate (t->left.op);
|
||||
tcl_iterate (t->right.key);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (term == NULL)
|
||||
error ("Cannot determine constrain level of empty term.");
|
||||
|
||||
vars = 0;
|
||||
structure = 0;
|
||||
flag = term_iterate_deVar (term, leaf, nodel, NULL, NULL);
|
||||
tcl_iterate (term);
|
||||
return ((float) vars / (float) structure);
|
||||
}
|
||||
|
||||
@ -170,7 +170,7 @@ float termDistance (Term t1, Term t2);
|
||||
int termOrder (Term t1, Term t2);
|
||||
int term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
|
||||
int (*nodem) (), int (*noder) ());
|
||||
int term_iterate_deVar (const Term term, int (*leaf) (), int (*nodel) (),
|
||||
int term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
|
||||
int (*nodem) (), int (*noder) ());
|
||||
int term_iterate_leaves (const Term t, int (*func) ());
|
||||
int term_iterate_open_leaves (const Term term, int (*func) ());
|
||||
|
||||
Loading…
Reference in New Issue
Block a user