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

Fixing read->recv conventions.

Browse Source
This commit is contained in:
Cas Cremers 2012-04-25 09:53:07 +02:00
parent 64e70ea4ea
commit 2242a5fcbd
18 changed files with 157 additions and 157 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
src/arachne.c
View File

@ -137,13 +137,13 @@ arachneInit (const System mysys)
add_event (SEND, NULL);
I_M = add_role ("I_M: Atomic message");
add_event (READ, NULL);
add_event (READ, NULL);
add_event (RECV, NULL);
add_event (RECV, NULL);
add_event (SEND, NULL);
I_RRS = add_role ("I_E: Encrypt");
add_event (READ, NULL);
add_event (READ, NULL);
add_event (RECV, NULL);
add_event (RECV, NULL);
add_event (SEND, NULL);
I_RRSD = add_role ("I_D: Decrypt");
@ -171,8 +171,8 @@ arachneDone ()
//! Just a defined integer for invalid
#define INVALID -1
//! can this roledef constitute a read Goal?
#define isGoal(rd) (rd->type == READ && !rd->internal)
//! can this roledef constitute a recv Goal?
#define isGoal(rd) (rd->type == RECV && !rd->internal)
//! is this roledef already bound?
#define isBound(rd) (rd->bound)
@ -401,7 +401,7 @@ fixAgentKeylevels (void)
*@returns The number of goals added (for destructions)
*/
int
add_read_goals (const int run, const int old, const int new)
add_recv_goals (const int run, const int old, const int new)
{
if (new <= sys->runs[run].height)
{
@ -419,7 +419,7 @@ add_read_goals (const int run, const int old, const int new)
count = 0;
while (i < new && rd != NULL)
{
if (rd->type == READ)
if (rd->type == RECV)
{
if (switches.output == PROOF)
{
@ -661,7 +661,7 @@ iterate_role_sends (int (*func) ())
//! Create decryption role instance
/**
* Note that this does not add any bindings for the reads.
* Note that this does not add any bindings for the receives.
*
*@param term The term to be decrypted (implies decryption key)
*@param key The key that is needed to decrypt the term
@ -902,9 +902,9 @@ bind_existing_to_goal (const Binding b, const int run, const int index,
return true;
}
// We need some adapting because the height would increase; we therefore
// have to add read goals before we know whether it unifies.
// have to add recv goals before we know whether it unifies.
old_length = sys->runs[run].height;
newgoals = add_read_goals (run, old_length, index + 1);
newgoals = add_recv_goals (run, old_length, index + 1);
{
// wrap substitution lists
@ -955,7 +955,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index,
int r2, e2;
r2 = TermRunid (tvar);
e2 = firstOccurrence (sys, r2, tsubst, READ);
e2 = firstOccurrence (sys, r2, tsubst, RECV);
if (e2 >= 0)
{
@ -1074,7 +1074,7 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
{
int newgoals;
newgoals = add_read_goals (run, 0, index + 1);
newgoals = add_recv_goals (run, 0, index + 1);
indentDepth++;
bind_existing_to_goal (b, run, index, true);
indentDepth--;
@ -1248,7 +1248,7 @@ bind_goal_new_encrypt (const Binding b)
{
int newgoals;
newgoals = add_read_goals (run, 0, index + 1);
newgoals = add_recv_goals (run, 0, index + 1);
{
indentDepth++;
@ -2283,7 +2283,7 @@ arachneClaimTest (Claimlist cl)
}
proof_suppose_run (run, 0, cl->ev + 1);
newgoals = add_read_goals (run, 0, cl->ev + 1);
newgoals = add_recv_goals (run, 0, cl->ev + 1);
/**
* Add initial knowledge node
@ -2499,7 +2499,7 @@ arachne ()
* completely ignores any information on unbound variables, and regards them
* as bound constants.
*
* Because everything is supposed to be bound, we conclude that even 'read'
* Because everything is supposed to be bound, we conclude that even 'recv'
* events imply a certain knowledge.
*
* If aftercomplete is 0 or false, we actually check the ordering; otherwise we
@ -2536,10 +2536,10 @@ knowledgeAtArachne (const System sys, const int myrun, const int myindex,
// Check whether this event precedes myevent
if (aftercomplete || isDependEvent (run, index, myrun, myindex))
{
// If it is a send (trivial) or a read (remarkable, but true
// If it is a send (trivial) or a recv (remarkable, but true
// because of bindings) we can add the message and the agents to
// the knowledge.
if (rd->type == SEND || rd->type == READ)
if (rd->type == SEND || rd->type == RECV)
{
knowledgeAddTerm (know, rd->message);
if (rd->from != NULL)

16
src/binding.c
View File

@ -295,7 +295,7 @@ goal_remove_last (int n)
}
}
//! Determine whether some label set is ordered w.r.t. send/read order.
//! Determine whether some label set is ordered w.r.t. send/recv order.
/**
* Assumes all these labels exist in the system, within length etc, and that the run mappings are valid.
*/
@ -304,9 +304,9 @@ labels_ordered (Termmap runs, Termlist labels)
{
while (labels != NULL)
{
// Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and readrole
// Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and recvrole
Labelinfo linfo;
int send_run, send_ev, read_run, read_ev;
int send_run, send_ev, recv_run, recv_ev;
int get_index (const int run)
{
@ -323,7 +323,7 @@ labels_ordered (Termmap runs, Termlist labels)
#ifdef DEBUG
if (rd == NULL)
error
("Could not locate send or read for label, after niagree holds, to test for order.");
("Could not locate send or recv for label, after niagree holds, to test for order.");
#endif
return i;
}
@ -332,10 +332,10 @@ labels_ordered (Termmap runs, Termlist labels)
if (!linfo->ignore)
{
send_run = termmapGet (runs, linfo->sendrole);
read_run = termmapGet (runs, linfo->readrole);
recv_run = termmapGet (runs, linfo->recvrole);
send_ev = get_index (send_run);
read_ev = get_index (read_run);
if (!isDependEvent (send_run, send_ev, read_run, read_ev))
recv_ev = get_index (recv_run);
if (!isDependEvent (send_run, send_ev, recv_run, recv_ev))
{
// Not ordered; false
return false;
@ -550,7 +550,7 @@ bindings_c_minimal ()
//!@todo hardcoded reference to step, should be length
for (ev = 0; ev < sys->runs[run].step; ev++)
{
if (rd->type == SEND || rd->type == READ)
if (rd->type == SEND || rd->type == RECV)
{
if (isDependEvent (run, ev, b->run_from, b->ev_from))
{

40
src/claim.c
View File

@ -129,14 +129,14 @@ events_match (const System sys, const int i, const int j)
isTermEqual (rdi->label, rdj->label) &&
!(rdi->internal || rdj->internal))
{
if (rdi->type == SEND && rdj->type == READ)
if (rdi->type == SEND && rdj->type == RECV)
{
if (i < j)
return MATCH_ORDER;
else
return MATCH_REVERSE;
}
if (rdi->type == READ && rdj->type == SEND)
if (rdi->type == RECV && rdj->type == SEND)
{
if (i > j)
return MATCH_ORDER;
@ -175,7 +175,7 @@ oki_nisynch_full (const System sys, const Termmap label_to_index)
return 1;
}
//! Evaluate claims or internal reads (chooses)
//! Evaluate claims or internal recvs (chooses)
__inline__ int
oki_nisynch_other (const System sys, const int trace_index,
const Termmap role_to_run, const Termmap label_to_index)
@ -196,13 +196,13 @@ oki_nisynch_other (const System sys, const int trace_index,
return result;
}
//! Evaluate reads
//! Evaluate recvs
__inline__ int
oki_nisynch_read (const System sys, const int trace_index,
oki_nisynch_recv (const System sys, const int trace_index,
const Termmap role_to_run, const Termmap label_to_index)
{
/*
* Read is only relevant for already involved runs, and labels in prec
* Recv is only relevant for already involved runs, and labels in prec
*/
Termmap role_to_run_scan;
int result = 7;
@ -228,7 +228,7 @@ oki_nisynch_read (const System sys, const int trace_index,
termmapSet (label_to_index_buf, rd->label, trace_index);
#ifdef OKIDEBUG
indact ();
eprintf ("Exploring because this (read) run is involved.\n");
eprintf ("Exploring because this (recv) run is involved.\n");
indac++;
#endif
result =
@ -248,7 +248,7 @@ oki_nisynch_read (const System sys, const int trace_index,
// Apparently not involved
#ifdef OKIDEBUG
indact ();
eprintf ("Exploring further assuming this (read) run is not involved.\n");
eprintf ("Exploring further assuming this (recv) run is not involved.\n");
indac++;
#endif
result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index);
@ -305,10 +305,10 @@ oki_nisynch_send (const System sys, const int trace_index,
// Was not involved yet in a registerd way, or was the correct rid
partner_index = termmapGet (label_to_index, rd->label);
// Ordered match needed for this label
// So it already needs to be filled by a read
// So it already needs to be filled by a recv
if (partner_index >= 0)
{
// There is already a read for it
// There is already a recv for it
if (events_match (sys, partner_index, trace_index) == MATCH_ORDER)
{
// They match in the right order
@ -385,12 +385,12 @@ oki_nisynch (const System sys, const int trace_index,
if (type == CLAIM || sys->traceEvent[trace_index]->internal)
return oki_nisynch_other (sys, trace_index, role_to_run, label_to_index);
if (type == READ)
return oki_nisynch_read (sys, trace_index, role_to_run, label_to_index);
if (type == RECV)
return oki_nisynch_recv (sys, trace_index, role_to_run, label_to_index);
if (type == SEND)
return oki_nisynch_send (sys, trace_index, role_to_run, label_to_index);
/*
* Exception: no claim, no send, no read, what is it?
* Exception: no claim, no send, no recv, what is it?
*/
error ("Unrecognized event type in claim scanner at %i.", trace_index);
return 0;
@ -540,8 +540,8 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs)
while (flag && labels != NULL)
{
// For each label, check whether it matches. Maybe a bit too strict (what about variables?)
// Locate roledefs for read & send, and check whether they are before step
Roledef rd_send, rd_read;
// Locate roledefs for recv & send, and check whether they are before step
Roledef rd_send, rd_recv;
Labelinfo linfo;
Roledef get_label_event (const Term role, const Term label)
@ -564,8 +564,8 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs)
eprintf ("\n");
eprintf ("This label has sendrole ");
termPrint (linfo->sendrole);
eprintf (" and readrole ");
termPrint (linfo->readrole);
eprintf (" and recvrole ");
termPrint (linfo->recvrole);
eprintf ("\n");
globalError--;
error ("Run mapping is out of bounds.");
@ -600,9 +600,9 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs)
if (!linfo->ignore)
{
rd_send = get_label_event (linfo->sendrole, labels->term);
rd_read = get_label_event (linfo->readrole, labels->term);
rd_recv = get_label_event (linfo->recvrole, labels->term);
if (rd_send == NULL || rd_read == NULL)
if (rd_send == NULL || rd_recv == NULL)
{
// False!
flag = 0;
@ -610,7 +610,7 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs)
else
{
// Compare
if (events_match_rd (rd_send, rd_read) != MATCH_CONTENT)
if (events_match_rd (rd_send, rd_recv) != MATCH_CONTENT)
{
// False!
flag = 0;

94
src/compiler.c
View File

@ -119,15 +119,15 @@ compilerDone (void)
return;
}
//! Compute read variables for a role
//! Compute recv variables for a role
Termlist
compute_read_variables (const Role r)
compute_recv_variables (const Role r)
{
Termlist tl;
int process_event (Roledef rd)
{
if (rd->type == READ)
if (rd->type == RECV)
{
tl = termlistAddVariables (tl, rd->from);
tl = termlistAddVariables (tl, rd->to);
@ -549,20 +549,20 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
if (claim == CLAIM_Secret)
{
Termlist claimvars;
Termlist readvars;
Termlist recvvars;
/* now check whether the claim contains variables that can actually be influenced by the intruder */
claimvars = termlistAddVariables (NULL, msg);
readvars = compute_read_variables (thisRole);
recvvars = compute_recv_variables (thisRole);
while (claimvars != NULL)
{
if (!inTermlist (protocol->rolenames, claimvars->term))
{
/* only if it is not a role */
if (!inTermlist (readvars, claimvars->term))
if (!inTermlist (recvvars, claimvars->term))
{
/* this claimvar does not occur in the reads? */
/* this claimvar does not occur in the recvs? */
/* then we should ignore it later */
cl->alwaystrue = true;
cl->warnings = true;
@ -574,14 +574,14 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
eprintf (" contains a variable ");
termPrint (claimvars->term);
eprintf
(" which is never read; therefore the claim will be true.\n");
(" which is never recv; therefore the claim will be true.\n");
globalError--;
}
}
claimvars = claimvars->next;
}
termlistDelete (claimvars);
termlistDelete (readvars);
termlistDelete (recvvars);
}
return cl;
}
@ -590,7 +590,7 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
void
commEvent (int event, Tac tc)
{
/* Add an event to the roledef, send or read */
/* Add an event to the roledef, send or recv */
Claimlist cl;
Term fromrole = NULL;
Term torole = NULL;
@ -606,8 +606,8 @@ commEvent (int event, Tac tc)
if (tc->t1.sym == NULL)
{
/* right, now this should not be NULL anyway, if so we construct a fresh one.
* This can be a weird choice if it is a read or send, because in that case
* we cannot chain them anymore and the send-read correspondence is lost.
* This can be a weird choice if it is a recv or send, because in that case
* we cannot chain them anymore and the send-recv correspondence is lost.
*/
int n;
Roledef rd;
@ -646,7 +646,7 @@ commEvent (int event, Tac tc)
trip = tc->t2.tac;
switch (event)
{
case READ:
case RECV:
case SEND:
/**
* We know the label. Find the corresponding labelinfo bit or make a new one
@ -687,18 +687,18 @@ commEvent (int event, Tac tc)
}
else
{
// READ
/* set readrole */
// RECV
/* set recvrole */
if (!isTermEqual (torole, thisRole->nameterm))
error
("Read role does not correspond to execution role at line %i.",
("Recv role does not correspond to execution role at line %i.",
tc->lineno);
if (linfo->readrole != NULL)
error ("Label defined twice for readrole!");
linfo->readrole = torole;
if (linfo->recvrole != NULL)
error ("Label defined twice for recvrole!");
linfo->recvrole = torole;
}
/* and make that read/send event */
/* and make that recv/send event */
thisRole->roledef = roledefAdd (thisRole->roledef, event, label,
fromrole, torole, msg, cl);
/* mark last one with line number */
@ -990,18 +990,18 @@ roleCompile (Term nameterm, Tac tc)
{
switch (tc->op)
{
case TAC_READ:
case TAC_RECV:
if (firstEvent)
{
// First a read, thus responder
// First a recv, thus responder
/*
* Semantics: defaults (in role.c) to initiator _unless_ the first event is a read,
* Semantics: defaults (in role.c) to initiator _unless_ the first event is a recv,
* in which case we assume that the agent names are possibly received as variables
*/
thisRole->initiator = 0;
firstEvent = 0;
}
commEvent (READ, tc);
commEvent (RECV, tc);
break;
case TAC_SEND:
firstEvent = 0;
@ -1412,7 +1412,7 @@ compute_label_roles (Termlist labels)
error ("Label in prec list not found in label info list");
#endif
roles = termlistAddNew (roles, linfo->sendrole);
roles = termlistAddNew (roles, linfo->readrole);
roles = termlistAddNew (roles, linfo->recvrole);
labels = labels->next;
}
@ -1479,8 +1479,8 @@ order_label_roles (const Claimlist cl)
}
}
roles_test (linfo->sendrole, linfo->readrole);
roles_test (linfo->readrole, linfo->sendrole);
roles_test (linfo->sendrole, linfo->recvrole);
roles_test (linfo->recvrole, linfo->sendrole);
}
}
return 1;
@ -1673,7 +1673,7 @@ compute_prec_sets (const System sys)
Roledef rd2;
rd2 = roledef_re (r2, ev2);
if (rd2 != NULL && rd2->type == READ
if (rd2 != NULL && rd2->type == RECV
&& isTermEqual (rd1->label, rd2->label))
{
SETBIT (prec + rowsize * index (r1, ev1),
@ -1769,9 +1769,9 @@ compute_prec_sets (const System sys)
{
// This event precedes the claim
if (rd->type == READ)
if (rd->type == RECV)
{
// Only store read labels (but send would work as well)
// Only store recv labels (but send would work as well)
cl->prec = termlistAdd (cl->prec, rd->label);
}
}
@ -1941,7 +1941,7 @@ checkRoleVariables (const System sys, const Protocol p, const Role r)
int process_event (Roledef rd)
{
if (rd->type == READ)
if (rd->type == RECV)
{
vars = termlistAddVariables (vars, rd->from);
vars = termlistAddVariables (vars, rd->to);
@ -1950,11 +1950,11 @@ checkRoleVariables (const System sys, const Protocol p, const Role r)
return 1;
}
/* Gather all variables occurring in the reads */
/* Gather all variables occurring in the recvs */
vars = NULL;
roledef_iterate_events (r->roledef, process_event);
/* Now, all variables for this role should be in the reads */
/* Now, all variables for this role should be in the recvs */
declared = r->declaredvars;
while (declared != NULL)
{
@ -1970,7 +1970,7 @@ checkRoleVariables (const System sys, const Protocol p, const Role r)
termPrint (p->nameterm);
eprintf (",");
termPrint (r->nameterm);
eprintf (" but never used in a read event.\n");
eprintf (" but never used in a recv event.\n");
globalError--;
}
}
@ -2081,13 +2081,13 @@ checkEventMatch (const Roledef rd1, const Roledef rd2,
return true;
}
//! Check label matchup for protocol p,r, roledef rd (which is a read)
//! Check label matchup for protocol p,r, roledef rd (which is a recv)
/**
* Any send with the same label should match
*/
void
checkLabelMatchThis (const System sys, const Protocol p, const Role readrole,
const Roledef readevent)
checkLabelMatchThis (const System sys, const Protocol p, const Role recvrole,
const Roledef recvevent)
{
Role sendrole;
int found;
@ -2103,13 +2103,13 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole,
{
if (event->type == SEND)
{
if (isTermEqual (event->label, readevent->label))
if (isTermEqual (event->label, recvevent->label))
{
// Same labels, so they should match up!
if (!checkEventMatch (event, readevent, p->rolenames))
if (!checkEventMatch (event, recvevent, p->rolenames))
{
globalError++;
eprintf ("error: [%i]", readevent->lineno);
eprintf ("error: [%i]", recvevent->lineno);
if (sys->protocols != NULL)
{
if (sys->protocols->next != NULL)
@ -2124,8 +2124,8 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole,
eprintf ("error: [%i] ", event->lineno);
roledefPrint (event);
eprintf (" does not match\n");
eprintf ("error: [%i] ", readevent->lineno);
roledefPrint (readevent);
eprintf ("error: [%i] ", recvevent->lineno);
roledefPrint (recvevent);
eprintf ("\n");
error_die ();
globalError--;
@ -2141,7 +2141,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole,
eprintf (" to match: ");
roledefPrint (event);
eprintf (" <> ");
roledefPrint (readevent);
roledefPrint (recvevent);
eprintf ("\n");
}
#endif
@ -2160,8 +2160,8 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole,
if (found == 0)
{
globalError++;
eprintf ("error: [%i] for the read event ", readevent->lineno);
roledefPrint (readevent);
eprintf ("error: [%i] for the recv event ", recvevent->lineno);
roledefPrint (recvevent);
eprintf (" of protocol ");
termPrint (p->nameterm);
eprintf
@ -2175,7 +2175,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole,
void
checkLabelMatchProtocol (const System sys, const Protocol p)
{
// For each read label the sends should match
// For each recv label the sends should match
Role r;
r = p->roles;
@ -2186,7 +2186,7 @@ checkLabelMatchProtocol (const System sys, const Protocol p)
rd = r->roledef;
while (rd != NULL)
{
if (rd->type == READ)
if (rd->type == RECV)
{
// We don't check all, if they start with a bang we ignore them.
Labelinfo li;

6
src/dotout.c
View File

@ -36,7 +36,7 @@ extern Role I_RRS;
extern Role I_RRSD;
#define INVALID -1
#define isGoal(rd) (rd->type == READ && !rd->internal)
#define isGoal(rd) (rd->type == RECV && !rd->internal)
#define isBound(rd) (rd->bound)
#define length step
@ -283,7 +283,7 @@ roledefDraw (Roledef rd)
}
}
if (rd->type == READ)
if (rd->type == RECV)
{
eprintf ("recv");
optlabel ();
@ -1244,7 +1244,7 @@ showLocal (const int run, Term told, Term tnew, char *prefix, char *cursep)
{
if (termOccursInRun (tnew, run))
{
// Variables are mapped, maybe. But then we wonder whether they occur in reads.
// Variables are mapped, maybe. But then we wonder whether they occur in recvs.
eprintf (cursep);
eprintf (prefix);
termPrintRemap (told);

2
src/label.c
View File

@ -53,7 +53,7 @@ label_create (const Term label, const Protocol protocol)
li->label = label;
li->protocol = protocol;
li->sendrole = NULL;
li->readrole = NULL;
li->recvrole = NULL;
// Should we ignore it?
li->ignore = false;
tl = rightMostTerm (label);

2
src/label.h
View File

@ -33,7 +33,7 @@ struct labelinfo
int ignore;
Protocol protocol;
Term sendrole;
Term readrole;
Term recvrole;
};
typedef struct labelinfo *Labelinfo;

4
src/parser.y
View File

@ -176,14 +176,14 @@ roledef : /* empty */
* but that will take a while I guess.
*/
event : READT label '(' termlist ')' ';'
{ Tac t = tacCreate(TAC_READ);
{ Tac t = tacCreate(TAC_RECV);
t->t1.sym = $2;
/* TODO test here: tac2 should have at least 3 elements */
t->t2.tac = $4;
$$ = t;
}
| RECVT label '(' termlist ')' ';'
{ Tac t = tacCreate(TAC_READ);
{ Tac t = tacCreate(TAC_RECV);
t->t1.sym = $2;
/* TODO test here: tac2 should have at least 3 elements */
t->t2.tac = $4;

2
src/prune_theorems.c
View File

@ -65,7 +65,7 @@ correctLocalOrder (const System sys)
e1 = firstOccurrence (sys, r1, t, ANYEVENT);
if (e1 >= 0)
{
if (roledef_shift (sys->runs[r1].start, e1)->type == READ)
if (roledef_shift (sys->runs[r1].start, e1)->type == RECV)
{
e2 = firstOccurrence (sys, r2, t, SEND);
if (e2 >= 0)

16
src/role.c
View File

@ -54,15 +54,15 @@ roledefPrintGeneric (Roledef rd, int print_actor)
eprintf ("[Empty roledef]");
return;
}
if (rd->type == READ && rd->internal)
if (rd->type == RECV && rd->internal)
{
/* special case: internal read == choose ! */
/* special case: internal recv == choose ! */
eprintf ("CHOOSE(");
termPrint (rd->message);
eprintf (")");
return;
}
if (rd->type == READ)
if (rd->type == RECV)
eprintf ("RECV");
if (rd->type == SEND)
eprintf ("SEND");
@ -93,14 +93,14 @@ roledefPrintGeneric (Roledef rd, int print_actor)
eprintf ("(");
if (!(rd->from == NULL && rd->to == NULL))
{
if (print_actor || rd->type == READ)
if (print_actor || rd->type == RECV)
{
termPrint (rd->from);
eprintf (",");
}
if (rd->type == CLAIM)
eprintf (" ");
if (print_actor || rd->type != READ)
if (print_actor || rd->type != RECV)
{
termPrint (rd->to);
eprintf (", ");
@ -205,7 +205,7 @@ roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl)
newEvent->forbidden = NULL; // no forbidden stuff
newEvent->knowPhase = -1; // we haven't explored any knowledge yet
newEvent->claiminfo = cl; // only for claims
if (type == READ)
if (type == RECV)
newEvent->bound = 0; // bound goal (Used for arachne only). Technically involves choose events as well.
else
newEvent->bound = 1; // other stuff does not need to be bound
@ -247,7 +247,7 @@ roleCreate (Term name)
r->variables = NULL;
r->declaredvars = NULL;
r->declaredconsts = NULL;
r->initiator = 1; //! Will be determined later, if a read is the first action (in compiler.c)
r->initiator = 1; //! Will be determined later, if a recv is the first action (in compiler.c)
r->singular = false; // by default, a role is not singular
r->next = NULL;
r->knows = NULL;
@ -470,7 +470,7 @@ WellFormedEvent (Term role, Knowledge know, Roledef rd)
{
return know;
}
if (rd->type == READ)
if (rd->type == RECV)
{
// Read
if (!isTermEqual (role, rd->to))

10
src/role.h
View File

@ -27,7 +27,7 @@
#include "states.h"
enum eventtype
{ READ, SEND, CLAIM, ANYEVENT };
{ RECV, SEND, CLAIM, ANYEVENT };
//! The container for the claim info list
/**
@ -88,13 +88,13 @@ struct roledef
{
//! flag for internal actions.
/**
* Typically, this is true to signify internal reads (e.g. variable choices)
* as opposed to a normal read.
* Typically, this is true to signify internal recvs (e.g. variable choices)
* as opposed to a normal recv.
*/
int internal;
//! Type of event.
/**
*\sa READ, SEND, CLAIM
*\sa RECV, SEND, CLAIM
*/
int type;
//! Event label.
@ -109,7 +109,7 @@ struct roledef
struct roledef *next;
/*
* Substructure for reads
* Substructure for recvs
*/
//! Illegal injections for this event.
/**

8
src/switches.c
View File

@ -104,7 +104,7 @@ switchesInit (int argc, char **argv)
switches.reportMemory = 0;
switches.reportTime = 0;
switches.countStates = false; // default off
switches.extendNonReads = 0; // default off
switches.extendNonRecvs = 0; // default off
switches.extendTrivial = 0; // default off
switches.plain = false; // default colors for terminal
switches.monochrome = false; // default colors for dot
@ -204,7 +204,7 @@ openFileSearch (char *filename, FILE * reopener)
if (switches.expert)
{
globalError++;
eprintf ("Reading file %s.\n", buffer);
eprintf ("Recving file %s.\n", buffer);
globalError--;
}
@ -987,7 +987,7 @@ switcher (const int process, int index, int commandline)
}
}
if (detect (' ', "extend-nonreads", 0))
if (detect (' ', "extend-nonrecvs", 0))
{
if (!process)
{
@ -996,7 +996,7 @@ switcher (const int process, int index, int commandline)
}
else
{
switches.extendNonReads = 1;
switches.extendNonRecvs = 1;
return index;
}
}

2
src/switches.h
View File

@ -80,7 +80,7 @@ struct switchdata
int reportMemory; //!< Memory display switch.
int reportTime; //!< Time display switch.
int countStates; //!< Count states
int extendNonReads; //!< Show further events in arachne xml output.
int extendNonRecvs; //!< Show further events in arachne xml output.
int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)
int plain; //!< Disable color output on terminal
int monochrome; //!< Disable colors in dot output

52
src/system.c
View File

@ -142,7 +142,7 @@ systemRuns (const System sys)
Roledef rd;
rd = runPointerGet (sys, run);
if (rd != NULL && rd->internal && rd->type == READ)
if (rd != NULL && rd->internal && rd->type == RECV)
{
/* increasing run traversal, so this yields max */
sys->lastChooseRun = run;
@ -243,7 +243,7 @@ ensureValidRun (const System sys, int run)
sys->runs[i].prevSymmRun = -1;
sys->runs[i].firstNonAgentRead = -1;
sys->runs[i].firstNonAgentRecv = -1;
sys->runs[i].firstReal = 0;
}
}
@ -283,13 +283,13 @@ runsPrint (const System sys)
}
}
//! Determine whether a term is sent or claimed, but not read first in a roledef
//! Determine whether a term is sent or claimed, but not recv first in a roledef
/**
* @returns True iff the term occurs, and is sent/claimed first. If this returns true,
* we have to prefix a read.
* we have to prefix a recv.
*/
int
not_read_first (const Roledef rdstart, const Term t)
not_recv_first (const Roledef rdstart, const Term t)
{
Roledef rd;
@ -298,12 +298,12 @@ not_read_first (const Roledef rdstart, const Term t)
{
if (termSubTerm (rd->message, t))
{
return (rd->type != READ);
return (rd->type != RECV);
}
rd = rd->next;
}
/* this term is not read or sent explicitly, which is no problem */
/* So we signal we don't have to prefix a read */
/* this term is not recv or sent explicitly, which is no problem */
/* So we signal we don't have to prefix a recv */
return 0;
}
@ -349,12 +349,12 @@ agentOfRun (const System sys, const int run)
return agentOfRunRole (sys, run, sys->runs[run].role->nameterm);
}
//! Determine first read with variables besides agents
//! Determine first recv with variables besides agents
/**
*@todo For now, we assume it is simply the first read after the choose, if there is one.
*@todo For now, we assume it is simply the first recv after the choose, if there is one.
*/
int
firstNonAgentRead (const System sys, int rid)
firstNonAgentRecv (const System sys, int rid)
{
int step;
Roledef rd;
@ -366,21 +366,21 @@ firstNonAgentRead (const System sys, int rid)
}
rd = sys->runs[rid].start;
step = 0;
while (rd != NULL && rd->internal && rd->type == READ) // assumes lazy LR eval
while (rd != NULL && rd->internal && rd->type == RECV) // assumes lazy LR eval
{
rd = rd->next;
step++;
}
if (rd != NULL && !rd->internal && rd->type == READ) // assumes lazy LR eval
if (rd != NULL && !rd->internal && rd->type == RECV) // assumes lazy LR eval
{
#ifdef DEBUG
warning
("First read %i with dependency on symmetrical found in run %i.",
("First recv %i with dependency on symmetrical found in run %i.",
step, rid);
#endif
return step;
}
/* no such read */
/* no such recv */
return -1;
}
@ -391,7 +391,7 @@ firstNonAgentRead (const System sys, int rid)
*
*************************************************/
//! Prefix a read before a given run.
//! Prefix a recv before a given run.
/**
* Maybe this simply needs integration in the role definitions. However, in practice it
* depends on the specific scenario. For Arachne it can thus depend on the roledef.
@ -399,15 +399,15 @@ firstNonAgentRead (const System sys, int rid)
* Stores the (new) rd pointer in start and index
*/
void
run_prefix_read (const System sys, const int run, Roledef rd,
run_prefix_recv (const System sys, const int run, Roledef rd,
const Term extterm)
{
/* prefix a read for such reads. TODO: this should also cover any external stuff */
/* prefix a recv for such recvs. TODO: this should also cover any external stuff */
if (extterm != NULL)
{
Roledef rdnew;
rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL);
rdnew = roledefInit (RECV, NULL, NULL, NULL, extterm, NULL);
/* this is an internal action! */
rdnew->internal = 1;
/* Store this new pointer */
@ -524,12 +524,12 @@ roleInstanceArachne (const System sys, const Protocol protocol,
TERMLISTAPPEND (runs[rid].rho, newt);
if (!role->initiator)
{
// For non-initiators, we prepend the reading of the role names
// For non-initiators, we prepend the recving of the role names
// XXX disabled for now TODO [x] [cc]
if (0 == 1 && not_read_first (rd, oldt))
if (0 == 1 && not_recv_first (rd, oldt))
{
/* this term is forced as a choose, or it does not occur in the (first) read event */
/* this term is forced as a choose, or it does not occur in the (first) recv event */
if (extterm == NULL)
{
extterm = newt;
@ -594,11 +594,11 @@ roleInstanceArachne (const System sys, const Protocol protocol,
createLocals (role->declaredvars, true, false);
createLocals (role->declaredconsts, false, false);
/* Now we prefix the read before rd, if extterm is not NULL. Even if
/* Now we prefix the recv before rd, if extterm is not NULL. Even if
* extterm is NULL, rd is still set as the start and the index pointer of
* the run.
*/
run_prefix_read (sys, rid, rd, extterm);
run_prefix_recv (sys, rid, rd, extterm);
/* TODO this is not what we want yet, also local knowledge. The local
* knowledge (list?) also needs to be substituted on invocation. */
@ -1131,7 +1131,7 @@ iterateLocalToOther (const System sys, const int myrun,
flag = true;
tlo = NULL;
// construct all others occuring in the reads
// construct all others occuring in the recvs
for (tls = sys->runs[myrun].sigma; tls != NULL; tls = tls->next)
{
Term tt;
@ -1181,7 +1181,7 @@ iterateRoles (const System sys, int (*callback) (Protocol p, Role r))
return true;
}
//! Get first read/send occurrence (event index) of term t in run r
//! Get first recv/send occurrence (event index) of term t in run r
int
firstOccurrence (const System sys, const int r, Term t, int evtype)
{

2
src/system.h
View File

@ -74,7 +74,7 @@ struct run
Termlist substitutions; //!< The substitutions as they came from the roledef unifier
int prevSymmRun; //!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter.
int firstNonAgentRead; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate.
int firstNonAgentRecv; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate.
int firstReal; //!< 1 if a choose was inserted, otherwise 0
};

4
src/tac.c
View File

@ -222,8 +222,8 @@ tacPrint (Tac t)
tacPrint (t->t2.tac);
printf ("};\n");
break;
case TAC_READ:
printf ("read");
case TAC_RECV:
printf ("recv");
if (t->t1.sym != NULL)
{
printf ("_%s", t->t1.sym->text);

2
src/tac.h
View File

@ -35,7 +35,7 @@ enum tactypes
TAC_VAR,
TAC_CONST,
TAC_FRESH,
TAC_READ,
TAC_RECV,
TAC_SEND,
TAC_CLAIM,
TAC_FUNC,

16
src/xmlout.c
View File

@ -525,7 +525,7 @@ isEventInteresting (const System sys, const Roledef rd)
/**
* run and index will only be output if they are nonnegative.
* Also prints any bindings, if this events follows some other events
* (typically when this is a read).
* (typically when this is a recv).
*
* If run < 0, it is assumed to be a role event, and thus no bindings will be shown.
*/
@ -542,10 +542,10 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
eprintf ("<event type=\"");
switch (rd->type)
{
/* Read or send types are fairly similar.
/* Recv or send types are fairly similar.
* Currently, choose events are not distinguished yet. TODO
*/
case READ:
case RECV:
eprintf ("recv");
break;
case SEND:
@ -566,7 +566,7 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
xmlOutTerm ("label", rd->label);
if (rd->type != CLAIM)
{
/* read or send */
/* recv or send */
xmlOutTerm ("from", rd->from);
xmlOutTerm ("to", rd->to);
xmlOutTerm ("message", rd->message);
@ -844,9 +844,9 @@ xmlOutRuns (const System sys)
}
else
{
if (switches.extendTrivial || switches.extendNonReads)
if (switches.extendTrivial || switches.extendNonRecvs)
{
if (rd->type != READ)
if (rd->type != RECV)
{
return true;
}
@ -854,7 +854,7 @@ xmlOutRuns (const System sys)
{
if (switches.extendTrivial)
{
/* This is a read, and we don't know whether to
/* This is a recv, and we don't know whether to
* include it. Default behaviour would be to jump
* out of the conditions, and return false.
* Instead, we check whether it can be trivially
@ -929,7 +929,7 @@ xmlOutSemitrace (const System sys)
eprintf ("<state");
/* add trace length attribute */
/* Note that this is the length of the attack leading up to the broken
* claim, thus without any run extensions (--extend-nonreads).
* claim, thus without any run extensions (--extend-nonrecvs).
*/
eprintf (" tracelength=\"%i\"", get_semitrace_length ());
/* add attack id attribute (within this scyther call) */