- Implemented --claim=ns3,I switch to filter certain claims.
This commit is contained in:
ccremers
parent
a6933806f9
commit
ec3be3d55b
200
src/arachne.c
200
src/arachne.c
@ -2238,129 +2238,125 @@ arachneClaim (Claimlist cl)
|
||||
// Skip the dummy claims
|
||||
if (!isTermEqual (cl->type, CLAIM_Empty))
|
||||
{
|
||||
// Any other claims might be filterered
|
||||
if (switches.filterClaim == NULL || switches.filterClaim == cl->type)
|
||||
// Some claims are always true!
|
||||
if (!cl->alwaystrue)
|
||||
{
|
||||
// Some claims are always true!
|
||||
if (!cl->alwaystrue)
|
||||
// others we simply test...
|
||||
int run;
|
||||
int newruns;
|
||||
Protocol p;
|
||||
Role r;
|
||||
|
||||
newruns = 0;
|
||||
sys->current_claim = cl;
|
||||
attack_length = INT_MAX;
|
||||
attack_leastcost = INT_MAX;
|
||||
cl->complete = 1;
|
||||
p = (Protocol) cl->protocol;
|
||||
r = (Role) cl->role;
|
||||
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
// others we simply test...
|
||||
int run;
|
||||
int newruns;
|
||||
Protocol p;
|
||||
Role r;
|
||||
indentPrint ();
|
||||
eprintf ("Testing Claim ");
|
||||
termPrint (cl->type);
|
||||
eprintf (" from ");
|
||||
termPrint (p->nameterm);
|
||||
eprintf (", ");
|
||||
termPrint (r->nameterm);
|
||||
eprintf (" at index %i.\n", cl->ev);
|
||||
}
|
||||
indentDepth++;
|
||||
|
||||
newruns = 0;
|
||||
sys->current_claim = cl;
|
||||
attack_length = INT_MAX;
|
||||
attack_leastcost = INT_MAX;
|
||||
cl->complete = 1;
|
||||
p = (Protocol) cl->protocol;
|
||||
r = (Role) cl->role;
|
||||
run = semiRunCreate (p, r);
|
||||
newruns++;
|
||||
{
|
||||
int newgoals;
|
||||
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Testing Claim ");
|
||||
termPrint (cl->type);
|
||||
eprintf (" from ");
|
||||
termPrint (p->nameterm);
|
||||
eprintf (", ");
|
||||
termPrint (r->nameterm);
|
||||
eprintf (" at index %i.\n", cl->ev);
|
||||
}
|
||||
indentDepth++;
|
||||
|
||||
run = semiRunCreate (p, r);
|
||||
newruns++;
|
||||
{
|
||||
int newgoals;
|
||||
|
||||
int realStart (void)
|
||||
{
|
||||
int realStart (void)
|
||||
{
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
printSemiState ();
|
||||
}
|
||||
#endif
|
||||
return iterate_buffer_attacks ();
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
printSemiState ();
|
||||
}
|
||||
#endif
|
||||
return iterate_buffer_attacks ();
|
||||
}
|
||||
|
||||
proof_suppose_run (run, 0, cl->ev + 1);
|
||||
newgoals = add_read_goals (run, 0, cl->ev + 1);
|
||||
proof_suppose_run (run, 0, cl->ev + 1);
|
||||
newgoals = add_read_goals (run, 0, cl->ev + 1);
|
||||
|
||||
/**
|
||||
* Add initial knowledge node
|
||||
*/
|
||||
{
|
||||
Termlist m0tl;
|
||||
Term m0t;
|
||||
int m0run;
|
||||
{
|
||||
Termlist m0tl;
|
||||
Term m0t;
|
||||
int m0run;
|
||||
|
||||
m0tl = knowledgeSet (sys->know);
|
||||
m0t = termlist_to_tuple (m0tl);
|
||||
// eprintf("Initial intruder knowledge node for ");
|
||||
// termPrint(m0t);
|
||||
// eprintf("\n");
|
||||
I_M->roledef->message = m0t;
|
||||
m0run = semiRunCreate (INTRUDER, I_M);
|
||||
newruns++;
|
||||
proof_suppose_run (m0run, 0, 1);
|
||||
sys->runs[m0run].height = 1;
|
||||
m0tl = knowledgeSet (sys->know);
|
||||
m0t = termlist_to_tuple (m0tl);
|
||||
// eprintf("Initial intruder knowledge node for ");
|
||||
// termPrint(m0t);
|
||||
// eprintf("\n");
|
||||
I_M->roledef->message = m0t;
|
||||
m0run = semiRunCreate (INTRUDER, I_M);
|
||||
newruns++;
|
||||
proof_suppose_run (m0run, 0, 1);
|
||||
sys->runs[m0run].height = 1;
|
||||
|
||||
{
|
||||
{
|
||||
/**
|
||||
* Add specific goal info and iterate algorithm
|
||||
*/
|
||||
add_claim_specifics (sys, cl,
|
||||
roledef_shift (sys->runs[run].
|
||||
start, cl->ev),
|
||||
realStart);
|
||||
}
|
||||
|
||||
|
||||
// remove initial knowledge node
|
||||
termDelete (m0t);
|
||||
termlistDelete (m0tl);
|
||||
semiRunDestroy ();
|
||||
newruns--;
|
||||
}
|
||||
// remove claiming run goals
|
||||
goal_remove_last (newgoals);
|
||||
semiRunDestroy ();
|
||||
newruns--;
|
||||
add_claim_specifics (sys, cl,
|
||||
roledef_shift (sys->runs[run].
|
||||
start, cl->ev),
|
||||
realStart);
|
||||
}
|
||||
//! Destroy
|
||||
while (sys->maxruns > 0 && newruns > 0)
|
||||
{
|
||||
semiRunDestroy ();
|
||||
newruns--;
|
||||
}
|
||||
|
||||
|
||||
// remove initial knowledge node
|
||||
termDelete (m0t);
|
||||
termlistDelete (m0tl);
|
||||
semiRunDestroy ();
|
||||
newruns--;
|
||||
}
|
||||
// remove claiming run goals
|
||||
goal_remove_last (newgoals);
|
||||
semiRunDestroy ();
|
||||
newruns--;
|
||||
}
|
||||
//! Destroy
|
||||
while (sys->maxruns > 0 && newruns > 0)
|
||||
{
|
||||
semiRunDestroy ();
|
||||
newruns--;
|
||||
}
|
||||
#ifdef DEBUG
|
||||
if (sys->bindings != NULL)
|
||||
{
|
||||
error ("sys->bindings NOT empty after claim test.");
|
||||
}
|
||||
if (sys->maxruns != 0)
|
||||
{
|
||||
error ("%i undestroyed runs left after claim test.",
|
||||
sys->maxruns);
|
||||
}
|
||||
if (newruns != 0)
|
||||
{
|
||||
error ("Lost %i runs after claim test.", newruns);
|
||||
}
|
||||
if (sys->bindings != NULL)
|
||||
{
|
||||
error ("sys->bindings NOT empty after claim test.");
|
||||
}
|
||||
if (sys->maxruns != 0)
|
||||
{
|
||||
error ("%i undestroyed runs left after claim test.",
|
||||
sys->maxruns);
|
||||
}
|
||||
if (newruns != 0)
|
||||
{
|
||||
error ("Lost %i runs after claim test.", newruns);
|
||||
}
|
||||
#endif
|
||||
|
||||
//! Indent back
|
||||
indentDepth--;
|
||||
//! Indent back
|
||||
indentDepth--;
|
||||
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Proof complete for this claim.\n");
|
||||
}
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
indentPrint ();
|
||||
eprintf ("Proof complete for this claim.\n");
|
||||
}
|
||||
}
|
||||
claimStatusReport (sys, cl);
|
||||
|
||||
@ -1,6 +1,7 @@
|
||||
#include <stdlib.h>
|
||||
#include <stdio.h>
|
||||
#include <limits.h>
|
||||
#include <string.h>
|
||||
#include "tac.h"
|
||||
#include "term.h"
|
||||
#include "termlist.h"
|
||||
@ -431,11 +432,31 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
|
||||
Claimlist cl;
|
||||
Term labeltuple;
|
||||
|
||||
/* check for ignored claim types */
|
||||
if (switches.filterClaim != NULL && switches.filterClaim != claim)
|
||||
if (switches.filterProtocol != NULL)
|
||||
{
|
||||
/* abort the construction of the node */
|
||||
return;
|
||||
// only this protocol
|
||||
if (strcmp
|
||||
(switches.filterProtocol, TermSymb (protocol->nameterm)->text) != 0)
|
||||
{
|
||||
// not this protocol; return
|
||||
return NULL;
|
||||
}
|
||||
// and maybe also a specific label?
|
||||
if (switches.filterLabel != NULL)
|
||||
{
|
||||
Term t;
|
||||
|
||||
t = label;
|
||||
while (isTermTuple (t))
|
||||
{
|
||||
t = TermOp2 (t);
|
||||
}
|
||||
if (strcmp (switches.filterLabel, TermSymb (t)->text) != 0)
|
||||
{
|
||||
// not this label; return
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* generate full unique label */
|
||||
@ -556,16 +577,15 @@ commEvent (int event, Tac tc)
|
||||
/* effectively, labels are bound to the protocol */
|
||||
level--;
|
||||
/* leaves a garbage tuple. dunnoh what to do with it */
|
||||
label =
|
||||
makeTermTuple (thisProtocol->nameterm, levelConst (tc->t1.sym));
|
||||
label = levelConst (tc->t1.sym);
|
||||
level++;
|
||||
}
|
||||
else
|
||||
{
|
||||
/* leaves a garbage tuple. dunnoh what to do with it */
|
||||
label = makeTermTuple (thisProtocol->nameterm, label);
|
||||
}
|
||||
}
|
||||
label = makeTermTuple (thisProtocol->nameterm, label);
|
||||
|
||||
/**
|
||||
* Parse the specific event type
|
||||
@ -1017,17 +1037,28 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
|
||||
Protocol pr;
|
||||
Term t;
|
||||
|
||||
if (levelFind (prots, level) != NULL)
|
||||
{
|
||||
globalError++;
|
||||
eprintf ("error: Double declaration of protocol ");
|
||||
symbolPrint (prots);
|
||||
eprintf (" ");
|
||||
errorTac (tc->lineno);
|
||||
}
|
||||
/* make new (empty) current protocol with name */
|
||||
pr = protocolCreate (levelConst (prots));
|
||||
thisProtocol = pr;
|
||||
{
|
||||
// check for double name declarations
|
||||
Protocol prold;
|
||||
|
||||
prold = sys->protocols;
|
||||
while (prold != NULL)
|
||||
{
|
||||
if (isTermEqual (pr->nameterm, prold->nameterm))
|
||||
{
|
||||
globalError++;
|
||||
eprintf ("error: Double declaration of protocol ");
|
||||
symbolPrint (prots);
|
||||
eprintf (" ");
|
||||
errorTac (tc->lineno);
|
||||
}
|
||||
prold = prold->next;
|
||||
}
|
||||
}
|
||||
|
||||
/* add protocol to list */
|
||||
pr->next = sys->protocols;
|
||||
sys->protocols = pr;
|
||||
|
||||
@ -53,7 +53,8 @@ switchesInit (int argc, char **argv)
|
||||
switches.maxproofdepth = INT_MAX;
|
||||
switches.maxtracelength = INT_MAX;
|
||||
switches.runs = 5; // default is 5 for usability, but -r 0 or --maxruns=0 will set it back to INT_MAX
|
||||
switches.filterClaim = NULL; // default check all claims
|
||||
switches.filterProtocol = NULL; // default check all claims
|
||||
switches.filterLabel = NULL; // default check all claims
|
||||
switches.maxAttacks = 0; // no maximum default
|
||||
|
||||
// Arachne
|
||||
@ -299,6 +300,20 @@ switcher (const int process, int index, int commandline)
|
||||
arg_pointer = argv[index];
|
||||
}
|
||||
|
||||
//! Retrieve a (string) argument
|
||||
char *string_argument (void)
|
||||
{
|
||||
char *result;
|
||||
|
||||
if (arg_pointer == NULL)
|
||||
{
|
||||
error ("Argument expected.");
|
||||
}
|
||||
result = arg_pointer;
|
||||
arg_next ();
|
||||
return result;
|
||||
}
|
||||
|
||||
//! Parse an argument into an integer
|
||||
int integer_argument (void)
|
||||
{
|
||||
@ -480,6 +495,30 @@ switcher (const int process, int index, int commandline)
|
||||
}
|
||||
}
|
||||
|
||||
if (detect (' ', "claim", 1))
|
||||
{
|
||||
if (!process)
|
||||
{
|
||||
helptext ("--claim=<protocol>[,<label>]",
|
||||
"check only a certain claim");
|
||||
}
|
||||
else
|
||||
{
|
||||
char *second;
|
||||
|
||||
switches.filterProtocol = string_argument ();
|
||||
second = strchr (switches.filterProtocol, ',');
|
||||
if (second != NULL)
|
||||
{
|
||||
// Cut off first part (turn ',' into '\0'; string is disposable) and proceed to next character.
|
||||
second[0] = '\0';
|
||||
second++;
|
||||
switches.filterLabel = second;
|
||||
}
|
||||
return index;
|
||||
}
|
||||
}
|
||||
|
||||
if (detect (' ', "remove-claims", 0))
|
||||
{
|
||||
if (!process)
|
||||
|
||||
@ -23,7 +23,8 @@ struct switchdata
|
||||
int maxproofdepth; //!< Maximum proof depth
|
||||
int maxtracelength; //!< Maximum trace length allowed
|
||||
int runs; //!< The number of runs as in the switch
|
||||
Term filterClaim; //!< Which claim should be checked?
|
||||
char *filterProtocol; //!< Which claim should be checked?
|
||||
char *filterLabel; //!< Which claim should be checked?
|
||||
int maxAttacks; //!< When not 0, maximum number of attacks
|
||||
|
||||
// Arachne
|
||||
|
||||
@ -1,9 +1,3 @@
|
||||
- Add --filter-claim and --filter-label switches; parse as symbols, and
|
||||
turn into (global?) terms, add to switches termlists. Later check them
|
||||
using two new term functions:
|
||||
const char *termSymbolString(Term t);
|
||||
int termSymbolEqual(Term t1, Term t2);
|
||||
Iteration through the termlist should be done by hand.
|
||||
- --check is slightly f***ed up because there is no good semantics for
|
||||
the --disable intruder check. As a result, it is now too strict can
|
||||
cause correct protocols to fail. Fix.
|
||||
|
||||
Loading…
Reference in New Issue
Block a user