Major:
- Added rho/sigma/constants fields to the runs, on which the new code is based. Over time, .locals should be deprecated in favour of these better variants. - Untyped variant is out of grace for the time being (cf. Athena interm problems) - Improved graph output further. Minor: - Added TERMLISTADD and APPEND macros for more concise code.
This commit is contained in:
ccremers
parent
5624f7e7b6
commit
1ce03104c5
@ -25,7 +25,7 @@ selfInitiator (const System sys, const int run)
|
||||
Termlist agents;
|
||||
Termlist seen;
|
||||
|
||||
agents = sys->runs[run].agents;
|
||||
agents = sys->runs[run].rho;
|
||||
seen = NULL;
|
||||
while (agents != NULL)
|
||||
{
|
||||
|
||||
225
src/dotout.c
225
src/dotout.c
@ -53,11 +53,36 @@ extern Role I_RRSD;
|
||||
* spread over all the runs.
|
||||
*/
|
||||
|
||||
static System sys = NULL;
|
||||
|
||||
/*
|
||||
* code
|
||||
*/
|
||||
|
||||
void
|
||||
printVisualRun (int rid)
|
||||
{
|
||||
int run;
|
||||
int display;
|
||||
|
||||
display = 1;
|
||||
for (run = 0; run < rid; run++)
|
||||
{
|
||||
if (sys->runs[run].protocol != INTRUDER)
|
||||
{
|
||||
display++;
|
||||
}
|
||||
}
|
||||
eprintf ("#%i", display);
|
||||
}
|
||||
|
||||
//! Remap term stuff
|
||||
void
|
||||
termPrintRemap (const Term t)
|
||||
{
|
||||
termPrintCustom (t, "", "V", "(", ")", "\\{ ", " \\}", printVisualRun);
|
||||
}
|
||||
|
||||
//! Draw node
|
||||
void
|
||||
node (const System sys, const int run, const int index)
|
||||
@ -113,7 +138,7 @@ roledefDraw (Roledef rd)
|
||||
label = TermOp2 (label);
|
||||
}
|
||||
eprintf ("_");
|
||||
termPrint (label);
|
||||
termPrintRemap (label);
|
||||
}
|
||||
}
|
||||
|
||||
@ -122,29 +147,29 @@ roledefDraw (Roledef rd)
|
||||
eprintf ("read");
|
||||
optlabel ();
|
||||
eprintf (" from ");
|
||||
termPrint (rd->from);
|
||||
termPrintRemap (rd->from);
|
||||
eprintf ("\\n");
|
||||
termPrint (rd->message);
|
||||
termPrintRemap (rd->message);
|
||||
}
|
||||
if (rd->type == SEND)
|
||||
{
|
||||
eprintf ("send");
|
||||
optlabel ();
|
||||
eprintf (" to ");
|
||||
termPrint (rd->to);
|
||||
termPrintRemap (rd->to);
|
||||
eprintf ("\\n");
|
||||
termPrint (rd->message);
|
||||
termPrintRemap (rd->message);
|
||||
}
|
||||
if (rd->type == CLAIM)
|
||||
{
|
||||
eprintf ("claim");
|
||||
optlabel ();
|
||||
eprintf ("\\n");
|
||||
termPrint (rd->to);
|
||||
termPrintRemap (rd->to);
|
||||
if (rd->message != NULL)
|
||||
{
|
||||
eprintf (" : ");
|
||||
termPrint (rd->message);
|
||||
termPrintRemap (rd->message);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -159,7 +184,7 @@ chooseTermNode (const Term t)
|
||||
|
||||
rsbuf = RUNSEP;
|
||||
RUNSEP = "x";
|
||||
termPrint (t);
|
||||
termPrintRemap (t);
|
||||
RUNSEP = rsbuf;
|
||||
}
|
||||
}
|
||||
@ -502,6 +527,27 @@ iterate_first_regular_occurrences (const System sys,
|
||||
return true;
|
||||
}
|
||||
|
||||
//! Does a term occur in a run?
|
||||
int
|
||||
termOccursInRun (Term t, int run)
|
||||
{
|
||||
Roledef rd;
|
||||
int e;
|
||||
|
||||
rd = sys->runs[run].start;
|
||||
e = 0;
|
||||
while (e < sys->runs[run].step)
|
||||
{
|
||||
if (roledefSubTerm (rd, t))
|
||||
{
|
||||
return true;
|
||||
}
|
||||
e++;
|
||||
rd = rd->next;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
//! Draw a class choice
|
||||
/**
|
||||
* \rho classes are already dealt with in the headers, so we should ignore them.
|
||||
@ -532,7 +578,7 @@ drawClass (const System sys, Binding b)
|
||||
run = TermRunid (varterm);
|
||||
if ((run >= 0) && (run < sys->maxruns))
|
||||
{
|
||||
if (inTermlist (sys->runs[run].agents, varterm))
|
||||
if (inTermlist (sys->runs[run].rho, varterm))
|
||||
{
|
||||
return;
|
||||
}
|
||||
@ -553,7 +599,7 @@ drawClass (const System sys, Binding b)
|
||||
eprintf ("\t");
|
||||
chooseTermNode (varterm);
|
||||
eprintf (" [label=\"Class:\\nAny ");
|
||||
termPrint (varterm);
|
||||
termPrintRemap (varterm);
|
||||
eprintf ("\"];\n");
|
||||
eprintf ("\t");
|
||||
chooseTermNode (varterm);
|
||||
@ -601,7 +647,7 @@ drawBinding (const System sys, Binding b)
|
||||
eprintf ("\t");
|
||||
arrow (sys, b);
|
||||
eprintf (" [label=\"");
|
||||
termPrint (b->term);
|
||||
termPrintRemap (b->term);
|
||||
eprintf ("\"]");
|
||||
eprintf (";\n");
|
||||
}
|
||||
@ -658,7 +704,7 @@ drawBinding (const System sys, Binding b)
|
||||
{
|
||||
// Only explicitly mention redirect term when it differs from the sent term
|
||||
eprintf ("\\n");
|
||||
termPrint (b->term);
|
||||
termPrintRemap (b->term);
|
||||
}
|
||||
eprintf ("\"]");
|
||||
eprintf (";\n");
|
||||
@ -720,14 +766,14 @@ agentsOfRunPrintOthers (const System sys, const int run)
|
||||
{
|
||||
Term agent;
|
||||
|
||||
termPrint (roles->term);
|
||||
termPrintRemap (roles->term);
|
||||
eprintf (" is ");
|
||||
agent = agentOfRunRole (sys, run, roles->term);
|
||||
if (isTermVariable (agent))
|
||||
{
|
||||
eprintf ("any ");
|
||||
}
|
||||
termPrint (agent);
|
||||
termPrintRemap (agent);
|
||||
eprintf ("\\l");
|
||||
}
|
||||
roles = roles->next;
|
||||
@ -767,7 +813,7 @@ drawRegularRuns (const System sys)
|
||||
eprintf ("\tsubgraph cluster_run%i {\n", run);
|
||||
eprintf ("\t\tlabel = \"");
|
||||
eprintf ("#%i: ", run);
|
||||
termPrint (sys->runs[run].protocol->nameterm);
|
||||
termPrintRemap (sys->runs[run].protocol->nameterm);
|
||||
eprintf (", ");
|
||||
agentsOfRunPrint (sys, run);
|
||||
eprintf ("\\nTesting the second line\";\n", run);
|
||||
@ -889,9 +935,9 @@ drawRegularRuns (const System sys)
|
||||
{
|
||||
eprintf ("Any ");
|
||||
}
|
||||
termPrint (agentname);
|
||||
termPrintRemap (agentname);
|
||||
eprintf (" in role ");
|
||||
termPrint (rolename);
|
||||
termPrintRemap (rolename);
|
||||
eprintf ("\\l");
|
||||
}
|
||||
|
||||
@ -953,27 +999,82 @@ drawRegularRuns (const System sys)
|
||||
if (showprotocol)
|
||||
{
|
||||
eprintf ("Protocol ");
|
||||
termPrint (sys->runs[run].protocol->
|
||||
nameterm);
|
||||
termPrintRemap (sys->runs[run].protocol->
|
||||
nameterm);
|
||||
eprintf ("\\l");
|
||||
}
|
||||
}
|
||||
eprintf ("Run #%i\\l", run);
|
||||
eprintf ("Run ");
|
||||
printVisualRun (run);
|
||||
eprintf ("\\l");
|
||||
|
||||
|
||||
// print the other agents
|
||||
eprintf ("|");
|
||||
if (termlistLength (sys->runs[run].agents) > 1)
|
||||
// rho, sigma, const
|
||||
void showLocal (Term told, Term tnew)
|
||||
{
|
||||
if (realTermVariable (tnew))
|
||||
{
|
||||
// Variables are mapped, maybe. But then we wonder whether they occur in reads.
|
||||
termPrintRemap (told);
|
||||
if (termOccursInRun (tnew, run))
|
||||
{
|
||||
eprintf (" : ");
|
||||
termPrintRemap (deVar (tnew));
|
||||
}
|
||||
else
|
||||
{
|
||||
eprintf (" is not read");
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
termPrintRemap (tnew);
|
||||
}
|
||||
eprintf ("\\l");
|
||||
}
|
||||
void showLocals (Termlist tlold, Termlist tlnew,
|
||||
Term tavoid)
|
||||
{
|
||||
while (tlold != NULL && tlnew != NULL)
|
||||
{
|
||||
if (!isTermEqual (tlold->term, tavoid))
|
||||
{
|
||||
showLocal (tlold->term, tlnew->term);
|
||||
}
|
||||
tlold = tlold->next;
|
||||
tlnew = tlnew->next;
|
||||
}
|
||||
}
|
||||
|
||||
if (termlistLength (sys->runs[run].rho) > 1)
|
||||
{
|
||||
eprintf ("|");
|
||||
if (sys->runs[run].role->initiator)
|
||||
{
|
||||
eprintf ("Chooses:\\l");
|
||||
eprintf ("Initiates with:\\l");
|
||||
}
|
||||
else
|
||||
{
|
||||
eprintf ("Assumes:\\l");
|
||||
eprintf ("Responds to:\\l");
|
||||
}
|
||||
agentsOfRunPrintOthers (sys, run);
|
||||
showLocals (sys->runs[run].protocol->
|
||||
rolenames, sys->runs[run].rho,
|
||||
sys->runs[run].role->nameterm);
|
||||
}
|
||||
|
||||
if (sys->runs[run].constants != NULL)
|
||||
{
|
||||
eprintf ("|Creates:\\l");
|
||||
showLocals (sys->runs[run].role->
|
||||
declaredconsts,
|
||||
sys->runs[run].constants, NULL);
|
||||
}
|
||||
if (sys->runs[run].sigma != NULL)
|
||||
{
|
||||
eprintf ("|Variables:\\l");
|
||||
showLocals (sys->runs[run].role->
|
||||
declaredvars,
|
||||
sys->runs[run].sigma, NULL);
|
||||
}
|
||||
|
||||
// close up
|
||||
@ -1113,7 +1214,7 @@ drawIntruderChoices (const System sys)
|
||||
eprintf ("\t");
|
||||
chooseTermNode (b->term);
|
||||
eprintf (" [label=\"Class: any ");
|
||||
termPrint (b->term);
|
||||
termPrintRemap (b->term);
|
||||
eprintf ("\",color=\"darkgreen\"];\n");
|
||||
|
||||
iterate_first_regular_occurrences (sys, firsthere, b->term);
|
||||
@ -1135,7 +1236,7 @@ drawIntruderChoices (const System sys)
|
||||
* This is not as nice as we would like it. Furthermore, the function is too big.
|
||||
*/
|
||||
void
|
||||
dotSemiState (const System sys)
|
||||
dotSemiState (const System mysys)
|
||||
{
|
||||
static int attack_number = 0;
|
||||
int run;
|
||||
@ -1145,16 +1246,18 @@ dotSemiState (const System sys)
|
||||
int from_intruder_count;
|
||||
int nodes;
|
||||
|
||||
sys = mysys;
|
||||
|
||||
// Open graph
|
||||
attack_number++;
|
||||
eprintf ("digraph semiState%i {\n", attack_number);
|
||||
eprintf ("\tlabel = \"[Id %i] Protocol ", sys->attackid);
|
||||
p = (Protocol) sys->current_claim->protocol;
|
||||
termPrint (p->nameterm);
|
||||
termPrintRemap (p->nameterm);
|
||||
eprintf (", role ");
|
||||
termPrint (sys->current_claim->rolename);
|
||||
termPrintRemap (sys->current_claim->rolename);
|
||||
eprintf (", claim type ");
|
||||
termPrint (sys->current_claim->type);
|
||||
termPrintRemap (sys->current_claim->type);
|
||||
eprintf ("\";\n");
|
||||
|
||||
// Globals
|
||||
@ -1242,39 +1345,41 @@ dotSemiState (const System sys)
|
||||
|
||||
// For debugging we might add more stuff: full dependencies
|
||||
#ifdef DEBUG
|
||||
{
|
||||
int r1;
|
||||
if (DEBUGL (3))
|
||||
{
|
||||
int r1;
|
||||
|
||||
for (r1 = 0; r1 < sys->maxruns; r1++)
|
||||
{
|
||||
if (sys->runs[r1].protocol != INTRUDER)
|
||||
{
|
||||
int e1;
|
||||
for (r1 = 0; r1 < sys->maxruns; r1++)
|
||||
{
|
||||
if (sys->runs[r1].protocol != INTRUDER)
|
||||
{
|
||||
int e1;
|
||||
|
||||
for (e1 = 0; e1 < sys->runs[r1].step; e1++)
|
||||
{
|
||||
int r2;
|
||||
for (e1 = 0; e1 < sys->runs[r1].step; e1++)
|
||||
{
|
||||
int r2;
|
||||
|
||||
for (r2 = 0; r2 < sys->maxruns; r2++)
|
||||
{
|
||||
if (sys->runs[r2].protocol != INTRUDER)
|
||||
{
|
||||
int e2;
|
||||
for (r2 = 0; r2 < sys->maxruns; r2++)
|
||||
{
|
||||
if (sys->runs[r2].protocol != INTRUDER)
|
||||
{
|
||||
int e2;
|
||||
|
||||
for (e2 = 0; e2 < sys->runs[r2].step; e2++)
|
||||
{
|
||||
if (isDependEvent (r1, e1, r2, e2))
|
||||
{
|
||||
eprintf ("\tr%ii%i -> r%ii%i [color=grey];\n",
|
||||
r1, e1, r2, e2);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
for (e2 = 0; e2 < sys->runs[r2].step; e2++)
|
||||
{
|
||||
if (isDependEvent (r1, e1, r2, e2))
|
||||
{
|
||||
eprintf
|
||||
("\tr%ii%i -> r%ii%i [color=grey];\n", r1,
|
||||
e1, r2, e2);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
// Intruder choices
|
||||
|
||||
@ -137,7 +137,7 @@ initiatorAgentsType (const System sys)
|
||||
{
|
||||
Termlist agents;
|
||||
|
||||
agents = sys->runs[run].agents;
|
||||
agents = sys->runs[run].rho;
|
||||
while (agents != NULL)
|
||||
{
|
||||
if (!goodAgentType (agents->term))
|
||||
@ -221,7 +221,7 @@ prune_theorems (const System sys)
|
||||
// Check this initiator run
|
||||
Termlist tl;
|
||||
|
||||
tl = sys->runs[run].agents;
|
||||
tl = sys->runs[run].rho;
|
||||
while (tl != NULL)
|
||||
{
|
||||
Termlist tlscan;
|
||||
@ -280,7 +280,7 @@ prune_theorems (const System sys)
|
||||
{
|
||||
if (sys->runs[run].protocol != INTRUDER)
|
||||
{
|
||||
if (sys->runs[run].agents != NULL)
|
||||
if (sys->runs[run].rho != NULL)
|
||||
{
|
||||
Term actor;
|
||||
|
||||
|
||||
268
src/system.c
268
src/system.c
@ -226,26 +226,27 @@ ensureValidRun (const System sys, int run)
|
||||
for (i = oldsize; i < sys->maxruns; i++)
|
||||
{
|
||||
/* init run */
|
||||
struct run myrun = sys->runs[i];
|
||||
myrun.protocol = NULL;
|
||||
myrun.role = NULL;
|
||||
myrun.agents = NULL;
|
||||
myrun.step = 0;
|
||||
myrun.index = NULL;
|
||||
myrun.start = NULL;
|
||||
sys->runs[i].protocol = NULL;
|
||||
sys->runs[i].role = NULL;
|
||||
sys->runs[i].step = 0;
|
||||
sys->runs[i].rolelength = 0;
|
||||
|
||||
myrun.rho = NULL;
|
||||
myrun.sigma = NULL;
|
||||
myrun.constants = NULL;
|
||||
myrun.locals = NULL;
|
||||
myrun.artefacts = NULL;
|
||||
myrun.substitutions = NULL;
|
||||
sys->runs[i].index = NULL;
|
||||
sys->runs[i].start = NULL;
|
||||
sys->runs[i].know = NULL;
|
||||
|
||||
myrun.know = NULL;
|
||||
sys->runs[i].rho = NULL;
|
||||
sys->runs[i].sigma = NULL;
|
||||
sys->runs[i].constants = NULL;
|
||||
|
||||
myrun.prevSymmRun = -1;
|
||||
myrun.firstNonAgentRead = -1;
|
||||
myrun.firstReal = 0;
|
||||
sys->runs[i].locals = NULL;
|
||||
sys->runs[i].artefacts = NULL;
|
||||
sys->runs[i].substitutions = NULL;
|
||||
|
||||
|
||||
sys->runs[i].prevSymmRun = -1;
|
||||
sys->runs[i].firstNonAgentRead = -1;
|
||||
sys->runs[i].firstReal = 0;
|
||||
}
|
||||
}
|
||||
|
||||
@ -321,7 +322,7 @@ agentOfRunRole (const System sys, const int run, const Term role)
|
||||
|
||||
// Agent variables have the same symbol as the role names, so
|
||||
// we can scan for this.
|
||||
agents = sys->runs[run].agents;
|
||||
agents = sys->runs[run].rho;
|
||||
while (agents != NULL)
|
||||
{
|
||||
Term agent;
|
||||
@ -367,7 +368,7 @@ staticRunSymmetry (const System sys, const int rid)
|
||||
|
||||
ridSymm = -1;
|
||||
runs = sys->runs;
|
||||
agents = runs[rid].agents;
|
||||
agents = runs[rid].rho;
|
||||
while (agents != NULL)
|
||||
{
|
||||
if (isTermVariable (agents->term))
|
||||
@ -378,7 +379,7 @@ staticRunSymmetry (const System sys, const int rid)
|
||||
if (ridSymm == -1)
|
||||
return -1;
|
||||
|
||||
agents = runs[rid].agents;
|
||||
agents = runs[rid].rho;
|
||||
while (ridSymm >= 0)
|
||||
{
|
||||
/* compare protocol name, role name */
|
||||
@ -391,7 +392,7 @@ staticRunSymmetry (const System sys, const int rid)
|
||||
|
||||
isEqual = 1;
|
||||
al = agents;
|
||||
alSymm = runs[ridSymm].agents;
|
||||
alSymm = runs[ridSymm].rho;
|
||||
while (isEqual && al != NULL)
|
||||
{
|
||||
/* determine equality */
|
||||
@ -572,7 +573,6 @@ run_localize (const System sys, const int rid, Termlist fromlist,
|
||||
}
|
||||
|
||||
|
||||
|
||||
//! Instantiate a role by making a new run for Arachne
|
||||
/**
|
||||
* This involves creation of a new run(id).
|
||||
@ -588,13 +588,8 @@ roleInstanceArachne (const System sys, const Protocol protocol,
|
||||
int rid;
|
||||
Run runs;
|
||||
Roledef rd;
|
||||
Termlist scanfrom, scanto;
|
||||
Termlist fromlist = NULL; // deleted at the end
|
||||
Termlist tolist = NULL; // -> .locals
|
||||
Termlist artefacts = NULL; // -> .artefacts
|
||||
Termlist rho = NULL; // -> .rho
|
||||
Termlist sigma = NULL; // -> .sigma
|
||||
Termlist constants = NULL; // -> .constants
|
||||
Term extterm = NULL; // construction thing (will go to artefacts)
|
||||
|
||||
/* claim runid, allocate space */
|
||||
@ -615,89 +610,95 @@ roleInstanceArachne (const System sys, const Protocol protocol,
|
||||
runs[rid].step = 0;
|
||||
runs[rid].firstReal = 0;
|
||||
|
||||
/* scan for types in agent list */
|
||||
/* scanners */
|
||||
/**
|
||||
* Because of pre-instantiation unification, some variables might already have been filled in.
|
||||
* Ignore agent list; instead rely on role->variables.
|
||||
/* Now we need to create local terms corresponding to rho, sigma, and any local constants.
|
||||
*
|
||||
* We maintain our stuff in a from/to list.
|
||||
*/
|
||||
runs[rid].agents = NULL;
|
||||
|
||||
scanfrom = role->variables;
|
||||
while (scanfrom != NULL)
|
||||
{
|
||||
Term newt, oldt;
|
||||
void createLocal (Term oldt, int isvariable, int isrole)
|
||||
{
|
||||
Term newt;
|
||||
|
||||
/* Some care has to be taken: after we use this instantiation, we might reset it.
|
||||
* That is not strictly necessary: whoever set it first, is responsible for getting rid
|
||||
* of it again.
|
||||
*/
|
||||
oldt = scanfrom->term;
|
||||
newt = deVar (oldt);
|
||||
if (realTermVariable (newt))
|
||||
{
|
||||
/* This is a variable of the role, that is not instantiated yet.
|
||||
* Thus, it needs a local copy.
|
||||
*/
|
||||
newt = makeTermType (VARIABLE, TermSymb (newt), rid);
|
||||
newt->stype = oldt->stype;
|
||||
artefacts = termlistAddNew (artefacts, newt);
|
||||
}
|
||||
/* Now we add any role names to the agent list. Note that
|
||||
* instantiations do not matter: because if the variable is
|
||||
* instantiated, the rolename will be as well, and thus they will be
|
||||
* equal anyway.
|
||||
*/
|
||||
if (inTermlist (protocol->rolenames, oldt))
|
||||
{
|
||||
/* Add the agent name or role variable... */
|
||||
runs[rid].agents = termlistAppend (runs[rid].agents, newt);
|
||||
// Create new term with the same symbol
|
||||
if (isvariable)
|
||||
{
|
||||
// Force variable
|
||||
newt = makeTermType (VARIABLE, TermSymb (oldt), rid);
|
||||
}
|
||||
else
|
||||
{
|
||||
// Force local (weirdly enough called global)
|
||||
newt = makeTermType (GLOBAL, TermSymb (oldt), rid);
|
||||
}
|
||||
newt->stype = oldt->stype; // copy list of types
|
||||
newt->roleVar = isrole; // set role status
|
||||
|
||||
if (isTermVariable (newt))
|
||||
{
|
||||
// It is a protocol role name
|
||||
// Add to copy list
|
||||
TERMLISTADD (fromlist, oldt);
|
||||
TERMLISTADD (tolist, newt);
|
||||
|
||||
// Flag this
|
||||
newt->roleVar = 1;
|
||||
newt->stype = termlistAddNew (newt->stype, TERM_Agent);
|
||||
// Add to registration lists
|
||||
// Everything to destructor list
|
||||
TERMLISTADD (runs[rid].artefacts, newt);
|
||||
// Variable / Constant?
|
||||
if (isvariable)
|
||||
{
|
||||
TERMLISTADD (sys->variables, newt);
|
||||
if (isrole)
|
||||
{
|
||||
// role variable
|
||||
/*
|
||||
* We use append to make sure the order is
|
||||
* consistent with the role names list.
|
||||
*/
|
||||
TERMLISTAPPEND (runs[rid].rho, newt);
|
||||
if (!role->initiator)
|
||||
{
|
||||
// For non-initiators, we prepend the reading of the role names
|
||||
|
||||
// maybe add choose?
|
||||
// Note that for anything but full type flaws, this is not an issue.
|
||||
// In the POR reduction, force choose was the default. Here it is not.
|
||||
/*
|
||||
* [x]
|
||||
* TODO currently disabled: something weird was goind on causing weird prunes,
|
||||
* for match=2. Investigate later.
|
||||
*/
|
||||
if (0 && not_read_first (rd, oldt) && switches.match == 2)
|
||||
{
|
||||
/* this term is forced as a choose, or it does not occur in the (first) read event */
|
||||
if (extterm == NULL)
|
||||
{
|
||||
extterm = newt;
|
||||
}
|
||||
else
|
||||
{
|
||||
extterm = makeTermTuple (newt, extterm);
|
||||
// NOTE: don't these get double deleted? By roledefdestroy?
|
||||
artefacts = termlistAddNew (artefacts, extterm);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
fromlist = termlistAdd (fromlist, oldt);
|
||||
tolist = termlistAdd (tolist, newt);
|
||||
// XXX disabled for now TODO [x] [cc]
|
||||
if (0 == 1 && not_read_first (rd, oldt))
|
||||
{
|
||||
/* this term is forced as a choose, or it does not occur in the (first) read event */
|
||||
if (extterm == NULL)
|
||||
{
|
||||
extterm = newt;
|
||||
}
|
||||
else
|
||||
{
|
||||
extterm = makeTermTuple (newt, extterm);
|
||||
// NOTE: don't these get double deleted? By roledefdestroy?
|
||||
TERMLISTAPPEND (runs[rid].artefacts, extterm);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// normal variable
|
||||
TERMLISTAPPEND (runs[rid].sigma, newt);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// local constant
|
||||
TERMLISTADD (runs[rid].constants, newt);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
eprintf ("Created for run %i: ", rid);
|
||||
termPrint (oldt);
|
||||
eprintf (" -> ");
|
||||
termPrint (newt);
|
||||
eprintf ("\n");
|
||||
*/
|
||||
void createLocals (Termlist list, int isvariable, int isrole)
|
||||
{
|
||||
while (list != NULL)
|
||||
{
|
||||
createLocal (list->term, isvariable, isrole);
|
||||
list = list->next;
|
||||
}
|
||||
}
|
||||
|
||||
scanfrom = scanfrom->next;
|
||||
}
|
||||
// Create rho, sigma, constants
|
||||
createLocals (protocol->rolenames, true, true);
|
||||
createLocals (role->declaredvars, true, false);
|
||||
createLocals (role->declaredconsts, false, false);
|
||||
|
||||
/* Now we prefix the read before rd, if extterm is not NULL. Even if
|
||||
* extterm is NULL, rd is still set as the start and the index pointer of
|
||||
@ -705,30 +706,6 @@ roleInstanceArachne (const System sys, const Protocol protocol,
|
||||
*/
|
||||
run_prefix_read (sys, rid, rd, extterm);
|
||||
|
||||
/* duplicate all locals form this run */
|
||||
scanto = role->locals;
|
||||
while (scanto != NULL)
|
||||
{
|
||||
Term t = scanto->term;
|
||||
if (!inTermlist (fromlist, t))
|
||||
{
|
||||
Term newt;
|
||||
|
||||
newt = create_new_local (t, rid);
|
||||
if (newt != NULL)
|
||||
{
|
||||
artefacts = termlistAddNew (artefacts, newt);
|
||||
if (realTermVariable (newt))
|
||||
{
|
||||
sys->variables = termlistAdd (sys->variables, newt);
|
||||
}
|
||||
fromlist = termlistAdd (fromlist, t);
|
||||
tolist = termlistAdd (tolist, newt);
|
||||
}
|
||||
}
|
||||
scanto = scanto->next;
|
||||
}
|
||||
|
||||
/* TODO this is not what we want yet, also local knowledge. The local
|
||||
* knowledge (list?) also needs to be substituted on invocation. */
|
||||
runs[rid].know = NULL;
|
||||
@ -738,7 +715,6 @@ roleInstanceArachne (const System sys, const Protocol protocol,
|
||||
|
||||
termlistDelete (fromlist);
|
||||
runs[rid].locals = tolist;
|
||||
runs[rid].artefacts = artefacts;
|
||||
|
||||
/* erase any substitutions in the role definition, as they are now copied */
|
||||
termlistSubstReset (role->variables);
|
||||
@ -795,6 +771,10 @@ roleInstanceDestroy (const System sys)
|
||||
|
||||
// Destroy artefacts
|
||||
//
|
||||
termlistDelete (myrun.rho);
|
||||
termlistDelete (myrun.sigma);
|
||||
termlistDelete (myrun.constants);
|
||||
|
||||
// sys->variables might contain locals from the run: remove them
|
||||
{
|
||||
Termlist tl;
|
||||
@ -822,19 +802,6 @@ roleInstanceDestroy (const System sys)
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
* Arachne does real-time reduction of memory, POR does not
|
||||
* Artefact removal can only be done if knowledge sets are empty, as with Arachne
|
||||
*/
|
||||
Termlist artefacts;
|
||||
// Remove artefacts
|
||||
artefacts = myrun.artefacts;
|
||||
while (artefacts != NULL)
|
||||
{
|
||||
free (artefacts->term);
|
||||
artefacts = artefacts->next;
|
||||
}
|
||||
|
||||
/**
|
||||
* Undo the local copies of the substitutions. We cannot restore them however, so this might
|
||||
* prove a problem. We assume that the substlist fixes this at roleInstance time; it should be exact.
|
||||
@ -854,10 +821,23 @@ roleInstanceDestroy (const System sys)
|
||||
}
|
||||
termlistDelete (myrun.substitutions);
|
||||
|
||||
/*
|
||||
* Artefact removal can only be done if knowledge sets are empty, as with Arachne
|
||||
*/
|
||||
{
|
||||
Termlist artefacts;
|
||||
// Remove artefacts
|
||||
artefacts = myrun.artefacts;
|
||||
while (artefacts != NULL)
|
||||
{
|
||||
free (artefacts->term);
|
||||
artefacts = artefacts->next;
|
||||
}
|
||||
}
|
||||
|
||||
// remove lists
|
||||
termlistDelete (myrun.artefacts);
|
||||
termlistDelete (myrun.locals);
|
||||
termlistDelete (myrun.agents);
|
||||
|
||||
// Destroy run struct allocation in array using realloc
|
||||
// Reduce run count
|
||||
@ -1059,7 +1039,7 @@ isRunTrusted (const System sys, const int run)
|
||||
{
|
||||
if (run >= 0 && run < sys->maxruns)
|
||||
{
|
||||
if (!isAgentlistTrusted (sys, sys->runs[run].agents))
|
||||
if (!isAgentlistTrusted (sys, sys->runs[run].rho))
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
@ -1192,7 +1172,7 @@ void
|
||||
runInstancePrint (const System sys, const int run)
|
||||
{
|
||||
termPrint (sys->runs[run].role->nameterm);
|
||||
termlistPrint (sys->runs[run].agents);
|
||||
termlistPrint (sys->runs[run].rho);
|
||||
}
|
||||
|
||||
//! Print an instantiated scenario (chooses and such)
|
||||
@ -1350,7 +1330,7 @@ iterateLocalToOther (const System sys, const int myrun,
|
||||
flag = true;
|
||||
tlo = NULL;
|
||||
// construct all others occuring in the reads
|
||||
for (tls = sys->runs[myrun].locals; tls != NULL; tls = tls->next)
|
||||
for (tls = sys->runs[myrun].sigma; tls != NULL; tls = tls->next)
|
||||
{
|
||||
Term tt;
|
||||
|
||||
|
||||
@ -41,18 +41,21 @@ struct run
|
||||
{
|
||||
Protocol protocol; //!< Protocol of this run.
|
||||
Role role; //!< Role of this run.
|
||||
Termlist agents; //!< Agents involved in this run.
|
||||
int step; //!< Current execution point in the run (integer)
|
||||
int rolelength; //!< Length of role
|
||||
|
||||
Roledef index; //!< Current execution point in the run (roledef pointer)
|
||||
Roledef start; //!< Head of the run definition.
|
||||
Knowledge know; //!< Current knowledge of the run.
|
||||
|
||||
Termlist rho; //!< As in semantics (copies in artefacts)
|
||||
Termlist sigma; //!< As in semantics (copies in artefacts)
|
||||
Termlist constants; //!< As in semantics (copies in artefacts)
|
||||
|
||||
Termlist locals; //!< Locals of the run (will be deprecated eventually)
|
||||
Termlist artefacts; //!< Stuff created especially for this run.
|
||||
Termlist artefacts; //!< Stuff created especially for this run, which can also include tuples (anything allocated)
|
||||
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 firstReal; //!< 1 if a choose was inserted, otherwise 0
|
||||
|
||||
@ -1,4 +1,5 @@
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
#include "tac.h"
|
||||
#include "memory.h"
|
||||
#include "switches.h"
|
||||
|
||||
66
src/term.c
66
src/term.c
@ -313,7 +313,9 @@ termInTerm (Term t, Term tsub)
|
||||
*\sa termTuplePrint()
|
||||
*/
|
||||
void
|
||||
termPrint (Term term)
|
||||
termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup,
|
||||
char *righttup, char *leftenc, char *rightenc,
|
||||
void (*callback) (int rid))
|
||||
{
|
||||
if (term == NULL)
|
||||
{
|
||||
@ -330,23 +332,34 @@ termPrint (Term term)
|
||||
#endif
|
||||
if (realTermLeaf (term))
|
||||
{
|
||||
if (term->type == VARIABLE && TermRunid (term) >= 0)
|
||||
eprintf (leftvar);
|
||||
symbolPrint (TermSymb (term));
|
||||
if (term->type == VARIABLE && TermRunid (term) >= 0)
|
||||
eprintf ("V");
|
||||
eprintf (rightvar);
|
||||
if (TermRunid (term) >= 0)
|
||||
{
|
||||
eprintf ("%s%i", RUNSEP, TermRunid (term));
|
||||
if (callback == NULL)
|
||||
{
|
||||
eprintf ("%s%i", RUNSEP, TermRunid (term));
|
||||
}
|
||||
else
|
||||
{
|
||||
callback (TermRunid (term));
|
||||
}
|
||||
}
|
||||
if (term->subst != NULL)
|
||||
{
|
||||
eprintf ("->");
|
||||
termPrint (term->subst);
|
||||
termPrintCustom (term->subst, leftvar, rightvar, lefttup, righttup,
|
||||
leftenc, rightenc, callback);
|
||||
}
|
||||
}
|
||||
if (realTermTuple (term))
|
||||
{
|
||||
eprintf ("(");
|
||||
termTuplePrint (term);
|
||||
termTuplePrintCustom (term, leftvar, rightvar, lefttup, righttup,
|
||||
leftenc, rightenc, callback);
|
||||
eprintf (")");
|
||||
return;
|
||||
}
|
||||
@ -356,22 +369,32 @@ termPrint (Term term)
|
||||
&& inTermlist (TermKey (term)->stype, TERM_Function))
|
||||
{
|
||||
/* function application */
|
||||
termPrint (TermKey (term));
|
||||
eprintf ("(");
|
||||
termTuplePrint (TermOp (term));
|
||||
eprintf (")");
|
||||
termPrintCustom (TermKey (term), leftvar, rightvar, lefttup,
|
||||
righttup, leftenc, rightenc, callback);
|
||||
eprintf (lefttup);
|
||||
termTuplePrintCustom (TermOp (term), leftvar, rightvar, lefttup,
|
||||
righttup, leftenc, rightenc, callback);
|
||||
eprintf (righttup);
|
||||
}
|
||||
else
|
||||
{
|
||||
/* normal encryption */
|
||||
eprintf ("{ ");
|
||||
termTuplePrint (TermOp (term));
|
||||
eprintf (" }");
|
||||
termPrint (TermKey (term));
|
||||
eprintf (leftenc);
|
||||
termTuplePrintCustom (TermOp (term), leftvar, rightvar, lefttup,
|
||||
righttup, leftenc, rightenc, callback);
|
||||
eprintf (rightenc);
|
||||
termPrintCustom (TermKey (term), leftvar, rightvar, lefttup,
|
||||
righttup, leftenc, rightenc, callback);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void
|
||||
termPrint (Term term)
|
||||
{
|
||||
termPrintCustom (term, "", "V", "(", ")", "{ ", " }", NULL);
|
||||
}
|
||||
|
||||
//! Print an inner (tuple) term to stdout, without brackets.
|
||||
/**
|
||||
* The tuple printing only works correctly for normalized terms.
|
||||
@ -379,7 +402,9 @@ termPrint (Term term)
|
||||
* desirable to distinguish them.
|
||||
*/
|
||||
void
|
||||
termTuplePrint (Term term)
|
||||
termTuplePrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup,
|
||||
char *righttup, char *leftenc, char *rightenc,
|
||||
void (*callback) (int rid))
|
||||
{
|
||||
if (term == NULL)
|
||||
{
|
||||
@ -390,14 +415,23 @@ termTuplePrint (Term term)
|
||||
while (realTermTuple (term))
|
||||
{
|
||||
// To remove any brackets, change this into termTuplePrint.
|
||||
termPrint (TermOp1 (term));
|
||||
termPrintCustom (TermOp1 (term), leftvar, rightvar, lefttup, righttup,
|
||||
leftenc, rightenc, callback);
|
||||
eprintf (",");
|
||||
term = deVar (TermOp2 (term));
|
||||
}
|
||||
termPrint (term);
|
||||
termPrintCustom (term, leftvar, rightvar, lefttup, righttup, leftenc,
|
||||
rightenc, callback);
|
||||
return;
|
||||
}
|
||||
|
||||
//! Print inner tuple
|
||||
void
|
||||
termTuplePrint (Term term)
|
||||
{
|
||||
termTuplePrintCustom (term, "", "V", "(", ")", "{ ", " }", NULL);
|
||||
}
|
||||
|
||||
//! Make a deep copy of a term.
|
||||
/**
|
||||
* Leaves are not copied.
|
||||
|
||||
@ -172,7 +172,13 @@ int hasTermVariable (Term term);
|
||||
int isTermEqualFn (Term term1, Term term2);
|
||||
int termSubTerm (Term t, Term tsub);
|
||||
int termInTerm (Term t, Term tsub);
|
||||
void termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup,
|
||||
char *righttup, char *leftenc, char *rightenc,
|
||||
void (*callback) (int rid));
|
||||
void termPrint (Term term);
|
||||
void termTuplePrintCustom (Term term, char *leftvar, char *rightvar,
|
||||
char *lefttup, char *righttup, char *leftenc,
|
||||
char *rightenc, void (*callback) (int rid));
|
||||
void termTuplePrint (Term term);
|
||||
Term termDuplicate (const Term term);
|
||||
Term termNodeDuplicate (const Term term);
|
||||
|
||||
@ -61,4 +61,7 @@ Term termlist_to_tuple (Termlist tl);
|
||||
Termlist tuple_to_termlist (Term t);
|
||||
Termlist termlistMinusTermlist (const Termlist tlbig, const Termlist tlsmall);
|
||||
|
||||
#define TERMLISTADD(l,t) l = termlistAdd (l,t)
|
||||
#define TERMLISTAPPEND(l,t) l = termlistAppend (l,t)
|
||||
|
||||
#endif
|
||||
|
||||
Loading…
Reference in New Issue
Block a user