- Bit masking was incorrect: & binds less strong than == !

This caused many of the --experimental switches not to work.
This commit is contained in:
ccremers 2006-02-28 13:41:36 +00:00
parent cf832ca1b1
commit 00616e45ed
5 changed files with 112 additions and 63 deletions

View File

@ -1645,7 +1645,7 @@ bind_goal_all_options (const Binding b)
} }
} }
if (switches.experimental & 4 == 0) if (switches.experimental & 4)
{ {
// Keylevel lemmas: improves on the previous one // Keylevel lemmas: improves on the previous one
if (!isPossiblySent (b->term)) if (!isPossiblySent (b->term))

View File

@ -108,7 +108,7 @@ prune_bounds (const System sys)
/** /**
* This should be removed once the hidelevel lemma works correctly * This should be removed once the hidelevel lemma works correctly
*/ */
if (switches.experimental & 4 == 0) if (switches.experimental & 4)
{ {
if ((switches.match < 2) if ((switches.match < 2)
&& (num_intruder_runs > && (num_intruder_runs >

View File

@ -12,6 +12,7 @@
#include "switches.h" #include "switches.h"
#include "binding.h" #include "binding.h"
#include "specialterm.h" #include "specialterm.h"
#include "hidelevel.h"
extern Protocol INTRUDER; extern Protocol INTRUDER;
extern int proofDepth; extern int proofDepth;
@ -25,6 +26,8 @@ extern int max_encryption_level;
int int
correctLocalOrder (const System sys) correctLocalOrder (const System sys)
{ {
int flag;
int checkRun (int r1) int checkRun (int r1)
{ {
int checkTerm (Term t) int checkTerm (Term t)
@ -37,31 +40,42 @@ correctLocalOrder (const System sys)
// t is a term from r2 that occurs in r1 // t is a term from r2 that occurs in r1
r2 = TermRunid (t); r2 = TermRunid (t);
e1 = firstOccurrence (sys, r1, t, READ); e1 = firstOccurrence (sys, r1, t, READ);
e2 = firstOccurrence (sys, r2, t, SEND); if (e1 >= 0)
// thus, it should not be the case that e1 occurs before e2
if (isDependEvent (r1, e1, r2, e2))
{ {
// That's not good! e2 = firstOccurrence (sys, r2, t, SEND);
if (switches.output == PROOF) if (e2 >= 0)
{ {
indentPrint ();
eprintf ("Pruned because ordering for term "); // thus, it should not be the case that e1 occurs before e2
termSubstPrint (t); if (isDependEvent (r1, e1, r2, e2))
eprintf {
(" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n", // That's not good!
r2, e2, r1, e1); if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Pruned because ordering for term ");
termSubstPrint (t);
eprintf
(" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n",
r2, e2, r1, e1);
}
flag = false;
return false;
}
} }
return false;
} }
} }
return true; return true;
} }
return iterateLocalToOther (sys, r1, checkTerm); return iterateLocalToOther (sys, r1, checkTerm);
} }
return iterateRegularRuns (sys, checkRun); flag = true;
iterateRegularRuns (sys, checkRun);
return flag;
} }
//! Check initiator roles //! Check initiator roles
@ -119,7 +133,7 @@ prune_theorems (const System sys)
eprintf eprintf
("Pruned because some local variable was incorrectly subsituted.\n"); ("Pruned because some local variable was incorrectly subsituted.\n");
} }
return 1; return true;
} }
// Check if all actors are agents for responders (initiators come next) // Check if all actors are agents for responders (initiators come next)
@ -140,7 +154,7 @@ prune_theorems (const System sys)
termPrint (actor); termPrint (actor);
eprintf (" of run %i is not of a compatible type.\n", run); eprintf (" of run %i is not of a compatible type.\n", run);
} }
return 1; return true;
} }
} }
run++; run++;
@ -179,7 +193,7 @@ prune_theorems (const System sys)
// Still need to fix proof output for this // Still need to fix proof output for this
// //
// Pruning because some agents are equal for this role. // Pruning because some agents are equal for this role.
return 1; return true;
} }
tlscan = tlscan->next; tlscan = tlscan->next;
} }
@ -199,7 +213,7 @@ prune_theorems (const System sys)
eprintf eprintf
("Pruned: an initiator role does not have the correct type for one of its agents.\n"); ("Pruned: an initiator role does not have the correct type for one of its agents.\n");
} }
return 1; return true;
} }
// Check if all agents of the main run are valid // Check if all agents of the main run are valid
@ -211,7 +225,7 @@ prune_theorems (const System sys)
eprintf eprintf
("Pruned because all agents of the claim run must be trusted.\n"); ("Pruned because all agents of the claim run must be trusted.\n");
} }
return 1; return true;
} }
// Check if the actors of all other runs are not untrusted // Check if the actors of all other runs are not untrusted
@ -242,7 +256,7 @@ prune_theorems (const System sys)
("Pruned because the actor of run %i is untrusted.\n", ("Pruned because the actor of run %i is untrusted.\n",
run); run);
} }
return 1; return true;
} }
} }
else else
@ -259,7 +273,7 @@ prune_theorems (const System sys)
eprintf ("\n"); eprintf ("\n");
error ("Aborting."); error ("Aborting.");
globalError--; globalError--;
return 1; return true;
} }
} }
run++; run++;
@ -275,16 +289,25 @@ prune_theorems (const System sys)
indentPrint (); indentPrint ();
eprintf ("Pruned because this is not <=c-minimal.\n"); eprintf ("Pruned because this is not <=c-minimal.\n");
} }
return 1; return true;
} }
} }
/* /*
* Check for correct orderings involving local constants * Check for correct orderings involving local constants
*/ */
if (switches.experimental & 8 != 0) if (switches.experimental & 8)
{ {
correctLocalOrder (sys); if (!correctLocalOrder (sys))
{
if (switches.output == PROOF)
{
indentPrint ();
eprintf
("Pruned because this does not have the correct local order.\n");
}
return true;
}
} }
/** /**
@ -297,7 +320,7 @@ prune_theorems (const System sys)
b = bl->data; b = bl->data;
if (switches.experimental & 4 == 0) if (switches.experimental & 4)
{ {
// Check for "Hidden" interm goals // Check for "Hidden" interm goals
//!@TODO in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs //!@TODO in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs
@ -311,35 +334,11 @@ prune_theorems (const System sys)
termPrint (b->term); termPrint (b->term);
eprintf ("\n"); eprintf ("\n");
} }
return 1; return true;
} }
} }
// Check for encryption levels if (switches.experimental & 4)
/*
* if (switches.match < 2
*!@TODO Doesn't work yet as desired for Tickets. Prove lemma first.
*/
if (switches.experimental & 2 > 0)
{
if (!hasTicketSubterm (b->term))
{
if (term_encryption_level (b->term) > max_encryption_level)
{
// Prune: we do not need to construct such terms
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Pruned because the encryption level of ");
termPrint (b->term);
eprintf (" is too high.\n");
}
return 1;
}
}
}
if (switches.experimental & 4 == 0)
{ {
// Check for SK-type function occurrences // Check for SK-type function occurrences
//!@todo Needs a LEMMA, although this seems to be quite straightforward to prove. //!@todo Needs a LEMMA, although this seems to be quite straightforward to prove.
@ -357,11 +356,51 @@ prune_theorems (const System sys)
termPrint (b->term); termPrint (b->term);
eprintf (" is not known initially to the intruder.\n"); eprintf (" is not known initially to the intruder.\n");
} }
return 1; return true;
} }
} }
} }
// Check for encryption levels
/*
* if (switches.match < 2
*!@TODO Doesn't work yet as desired for Tickets. Prove lemma first.
*/
if (switches.experimental & 2)
{
if (!hasTicketSubterm (b->term))
{
if (term_encryption_level (b->term) > max_encryption_level)
{
// Prune: we do not need to construct such terms
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Pruned because the encryption level of ");
termPrint (b->term);
eprintf (" is too high.\n");
}
return true;
}
}
}
/**
* Prune on the basis of hidelevel lemma
*/
if (hidelevelImpossible (sys, b->term))
{
// Prune: we do not need to construct such terms
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Pruned because the hidelevel of ");
termPrint (b->term);
eprintf (" is impossible to satisfy.\n");
}
return true;
}
bl = bl->next; bl = bl->next;
} }
@ -393,7 +432,7 @@ prune_theorems (const System sys)
termPrint (rolename); termPrint (rolename);
eprintf (" occurs more than once in the semitrace.\n"); eprintf (" occurs more than once in the semitrace.\n");
} }
return 1; return true;
} }
run2++; run2++;
} }
@ -401,5 +440,5 @@ prune_theorems (const System sys)
run++; run++;
} }
return 0; return false;
} }

View File

@ -1598,6 +1598,7 @@ iterateLocalToOther (const System sys, const int myrun,
int (*callback) (Term tlocal)) int (*callback) (Term tlocal))
{ {
Termlist tlo, tls; Termlist tlo, tls;
int flag;
int addOther (Term t) int addOther (Term t)
{ {
@ -1605,24 +1606,31 @@ iterateLocalToOther (const System sys, const int myrun,
return true; return true;
} }
flag = true;
tlo = NULL; tlo = NULL;
// construct all others occuring in the reads // construct all others occuring in the reads
for (tls = sys->runs[myrun].locals; tls != NULL; tls = tls->next) for (tls = sys->runs[myrun].locals; tls != NULL; tls = tls->next)
{ {
iterateTermOther (myrun, tls->term, addOther); Term tt;
tt = tls->term;
if (realTermVariable (tt) && tt->subst != NULL);
{
iterateTermOther (myrun, tt->subst, addOther);
}
} }
// now iterate over all of them // now iterate over all of them
for (tls = tlo; tls != NULL; tls = tls->next) for (tls = tlo; flag && (tls != NULL); tls = tls->next)
{ {
if (!callback (tls->term)) if (!callback (tls->term))
{ {
return false; flag = false;
} }
} }
// clean up // clean up
termlistDelete (tlo); termlistDelete (tlo);
return true; return flag;
} }
//! Get first read/send occurrence (event index) of term t in run r //! Get first read/send occurrence (event index) of term t in run r

View File

@ -992,14 +992,14 @@ term_iterate_deVar (Term term, int (*leaf) (Term t), int (*nodel) (Term t),
} }
else else
{ {
return 1; return true;
} }
} }
else else
{ {
int flag; int flag;
flag = 1; flag = true;
if (nodel != NULL) if (nodel != NULL)
flag = flag && nodel (term); flag = flag && nodel (term);
@ -1015,6 +1015,8 @@ term_iterate_deVar (Term term, int (*leaf) (Term t), int (*nodel) (Term t),
&& &&
(term_iterate_deVar (TermOp (term), leaf, nodel, nodem, noder)); (term_iterate_deVar (TermOp (term), leaf, nodel, nodem, noder));
// Center
if (nodem != NULL) if (nodem != NULL)
flag = flag && nodem (term); flag = flag && nodem (term);
@ -1036,7 +1038,7 @@ term_iterate_deVar (Term term, int (*leaf) (Term t), int (*nodel) (Term t),
return flag; return flag;
} }
} }
return 1; return true;
} }
//! Iterate over the leaves in a term //! Iterate over the leaves in a term