scyther/src/knowledge.c

551 lines
12 KiB
C
Raw Normal View History

2004-05-15 15:22:44 +01:00
/**
*@file knowledge.c
*\brief Procedures concerning knowledge structures.
*
* The main issue of this code is to maintain the minimal property of the knowledge set.
*/
2004-04-23 11:58:43 +01:00
#include <stdlib.h>
#include <stdio.h>
#include "termlist.h"
2004-04-23 11:58:43 +01:00
#include "knowledge.h"
#include "memory.h"
#include "system.h"
2004-04-23 11:58:43 +01:00
#include "debug.h"
/*
* Knowledge stuff
*
* Note that a really weird thing is going on involving unpropagated substitutions.
* Idea:
*
* 1. Substitute terms by filling in ->subst.
* Now, either:
* 2a. Undo this by knowledgeUndo.
* 2b. Propagate it, modifying the knowledge beyond repair by knowledgeSubstDo. Now inKnowledge works again.
* 2c. inKnowledge/knowledgeSet if something is in the knowledge: this does not consider the substitutions!, and
* they now have some overhead.
*/
2004-05-15 15:22:44 +01:00
//! Open knowledge code.
2004-04-23 11:58:43 +01:00
void
knowledgeInit (void)
{
return;
}
2004-05-15 15:22:44 +01:00
//! Close knowledge code.
2004-04-23 11:58:43 +01:00
void
knowledgeDone (void)
{
}
2004-05-15 15:22:44 +01:00
//! Allocate a fresh memory block the size of a knowledge struct.
/**
* Memory will not be initialized.
*@return Pointer to a fresh memory block.
*/
2004-04-23 11:58:43 +01:00
Knowledge
makeKnowledge ()
{
return (Knowledge) memAlloc (sizeof (struct knowledge));
}
2004-05-15 15:22:44 +01:00
//! Create a new empty knowledge structure.
/**
*@return Pointer to an empty knowledge structure.
*/
2004-04-23 11:58:43 +01:00
Knowledge
emptyKnowledge ()
{
Knowledge know;
know = makeKnowledge ();
know->basic = NULL;
know->encrypt = NULL;
know->inverses = NULL;
know->vars = NULL;
return know;
}
2004-05-15 15:22:44 +01:00
//! Duplicate a knowledge structure.
/**
* Makes copies using termlistShallow() of knowledge::basic, knowledge::encrypt and
* knowledge::vars.
* For the inverses, only the pointer is copied.
*@param know The knowledge structure to be copied.
*@return A pointer to a new memory struct.
*\sa termlistShallow(), knowledgeDelete()
*/
2004-04-23 11:58:43 +01:00
Knowledge
knowledgeDuplicate (Knowledge know)
{
Knowledge newknow;
if (know == NULL)
{
warning ("Trying to copy empty knowledge.");
2004-04-23 11:58:43 +01:00
return NULL;
}
newknow = makeKnowledge ();
newknow->basic = termlistShallow (know->basic);
newknow->encrypt = termlistShallow (know->encrypt);
newknow->vars = termlistShallow (know->vars);
newknow->inverses = know->inverses;
return newknow;
}
2004-05-15 15:22:44 +01:00
//! Delete a knowledge set.
/**
* Typically used to destroy something made with knowledgeDuplicate().
*\sa knowledgeDuplicate()
*/
2004-04-23 11:58:43 +01:00
void
knowledgeDelete (Knowledge know)
{
if (know != NULL)
{
termlistDelete (know->basic);
termlistDelete (know->encrypt);
termlistDelete (know->vars);
memFree (know, sizeof (struct knowledge));
}
}
2004-05-15 15:22:44 +01:00
//! Destroy a knowledge set.
/**
* Unlike knowledgeDelete(), uses termlistDestroy() to remove knowledge::basic,
* knowledge::encrypt and knowledge::vars substructures.
*\sa knowledgeDelete()
*/
2004-04-23 11:58:43 +01:00
void
knowledgeDestroy (Knowledge know)
{
if (know != NULL)
{
termlistDestroy (know->basic);
termlistDestroy (know->encrypt);
termlistDestroy (know->vars);
// termlistDestroy(know->inverses);
memFree (know, sizeof (struct knowledge));
}
}
2004-05-15 15:22:44 +01:00
//! Add a term to a knowledge set.
/**
*@param know The knowledge set.
*@param term The term to be added.
*@return True iff the term was actually new, and added.
2004-04-23 11:58:43 +01:00
*/
int
knowledgeAddTerm (Knowledge know, Term term)
{
if (know == NULL)
{
warning ("Trying to add term to uninitialised (NULL) Know pointer.");
2004-04-23 11:58:43 +01:00
return 1;
}
if (term == NULL)
return 0;
term = deVar (term);
/* for tuples, simply recurse for components */
2004-04-23 11:58:43 +01:00
if (isTermTuple (term))
{
int status;
2004-11-16 12:07:55 +00:00
status = knowledgeAddTerm (know, TermOp1 (term));
return knowledgeAddTerm (know, TermOp2 (term)) || status;
2004-04-23 11:58:43 +01:00
}
/* test whether we knew it before */
if (inKnowledge (know, term))
return 0;
2004-04-23 11:58:43 +01:00
/* adding variables? */
know->vars = termlistAddVariables (know->vars, term);
knowledgeSimplify (know, term);
if (isTermLeaf (term))
{
know->basic = termlistAdd (know->basic, term);
}
if (term->type == ENCRYPT)
{
2004-11-16 12:07:55 +00:00
Term invkey = inverseKey (know->inverses, TermKey (term));
2004-04-23 11:58:43 +01:00
if (inKnowledge (know, invkey))
{
/* we can decrypt it */
2004-11-16 12:07:55 +00:00
knowledgeAddTerm (know, TermOp (term));
if (!inKnowledge (know, TermKey (term)))
2004-04-23 11:58:43 +01:00
{
/* we know the op now, but not the key, so add it anyway */
know->encrypt = termlistAdd (know->encrypt, term);
}
}
else
{
/* we cannot decrypt it, and from the initial test we know we could not construct it */
know->encrypt = termlistAdd (know->encrypt, term);
}
termDelete (invkey);
}
return 1;
}
2004-05-15 15:22:44 +01:00
//! Try to simplify knowledge based on a term.
/**
*@param know A knowledge set.
2004-06-13 21:58:54 +01:00
*@param key A key, i.e. it can decrypt anything that was encrypted with term^{-1}.
2004-05-15 15:22:44 +01:00
*/
2004-04-23 11:58:43 +01:00
void
knowledgeSimplify (Knowledge know, Term key)
{
Termlist tldecrypts = NULL;
Termlist scan = know->encrypt;
Term invkey = inverseKey (know->inverses, key);
while (scan != NULL)
{
2004-11-16 12:07:55 +00:00
if (isTermEqual (TermKey (scan->term), invkey))
2004-04-23 11:58:43 +01:00
{
2004-11-16 12:07:55 +00:00
tldecrypts = termlistAdd (tldecrypts, TermOp (scan->term));
2004-04-23 11:58:43 +01:00
know->encrypt = termlistDelTerm (scan);
scan = know->encrypt;
}
else
scan = scan->next;
}
termDelete (invkey);
knowledgeAddTermlist (know, tldecrypts);
termlistDelete (tldecrypts);
}
2004-05-15 15:22:44 +01:00
//! Add a termlist to the knowledge.
2004-04-23 11:58:43 +01:00
/*
2004-05-15 15:22:44 +01:00
*@return True iff there was at least one new item.
*\sa knowledgeAddTerm()
2004-04-23 11:58:43 +01:00
*/
int
knowledgeAddTermlist (Knowledge know, Termlist tl)
{
int flag = 0;
while (tl != NULL)
{
flag = knowledgeAddTerm (know, tl->term) || flag;
tl = tl->next;
}
return flag;
}
2004-05-15 15:22:44 +01:00
//! Add an inverse pair to the knowledge
2004-04-23 11:58:43 +01:00
void
knowledgeAddInverse (Knowledge know, Term t1, Term t2)
{
know->inverses = termlistAdd (know->inverses, t1);
know->inverses = termlistAdd (know->inverses, t2);
return;
}
2004-05-15 15:22:44 +01:00
//! Set an inverse pair list for the knowledge.
/**
* List pointer is simply copied, so don't delete it later!
*/
2004-04-23 11:58:43 +01:00
void
knowledgeSetInverses (Knowledge know, Termlist tl)
{
know->inverses = tl;
}
2004-05-15 15:22:44 +01:00
//! Is a term a part of the knowledge?
/**
*@param know The knowledge set.
*@param term The term to be inferred.
*@return True iff the term can be inferred from the knowledge set.
*/
2004-04-23 11:58:43 +01:00
int
inKnowledge (const Knowledge know, Term term)
{
2004-05-26 13:17:09 +01:00
mindwipe (know, inKnowledge (know, term));
2004-04-23 11:58:43 +01:00
/* if there is no term, then it's okay 'fur sure' */
if (term == NULL)
return 1;
/* if there is a term, but no knowledge, we're in trouble */
if (know == NULL)
return 0;
term = deVar (term);
if (isTermLeaf (term))
{
return inTermlist (know->basic, term);
}
if (term->type == ENCRYPT)
{
return inTermlist (know->encrypt, term) ||
2004-11-16 12:07:55 +00:00
(inKnowledge (know, TermKey (term))
&& inKnowledge (know, TermOp (term)));
2004-04-23 11:58:43 +01:00
}
if (term->type == TUPLE)
{
return (inTermlist (know->encrypt, term) ||
2004-11-16 12:07:55 +00:00
(inKnowledge (know, TermOp1 (term)) &&
inKnowledge (know, TermOp2 (term))));
2004-04-23 11:58:43 +01:00
}
return 0; /* unrecognized term type, weird */
}
2004-05-15 15:22:44 +01:00
//! Compare two knowledge sets.
/**
* This does not check currently for equivalence of inverse sets, which it should.
*@return True iff both knowledge sets are equal.
*/
2004-04-23 11:58:43 +01:00
int
isKnowledgeEqual (Knowledge know1, Knowledge know2)
{
if (know1 == NULL || know2 == NULL)
{
if (know1 == NULL && know2 == NULL)
return 1;
else
return 0;
}
if (!isTermlistEqual (know1->encrypt, know2->encrypt))
return 0;
return isTermlistEqual (know1->basic, know2->basic);
}
2004-05-15 15:22:44 +01:00
//! Print a knowledge set.
2004-04-23 11:58:43 +01:00
void
knowledgePrint (Knowledge know)
{
indent ();
if (know == NULL)
{
eprintf ("Empty.\n");
2004-04-23 11:58:43 +01:00
return;
}
eprintf (" [Basic]: ");
2004-04-23 11:58:43 +01:00
termlistPrint (know->basic);
eprintf ("\n");
2004-04-23 11:58:43 +01:00
indent ();
eprintf (" [Encrp]: ");
2004-04-23 11:58:43 +01:00
termlistPrint (know->encrypt);
eprintf ("\n");
2004-04-23 11:58:43 +01:00
indent ();
eprintf (" [Vars]: ");
2004-04-23 11:58:43 +01:00
termlistPrint (know->vars);
eprintf ("\n");
2004-04-23 11:58:43 +01:00
}
//! Print a knowledge set, short version (no newline)
void
knowledgePrintShort (const Knowledge know)
{
indent ();
if (know == NULL)
{
eprintf ("Empty");
return;
}
if (know->basic != NULL)
{
termlistPrint (know->basic);
if (know->encrypt != NULL);
{
eprintf (", ");
}
}
if (know->encrypt != NULL)
{
termlistPrint (know->encrypt);
}
}
2004-05-15 15:22:44 +01:00
//! Print the inverses list of a knowledge set.
2004-04-23 11:58:43 +01:00
void
knowledgeInversesPrint (Knowledge know)
{
Termlist tl;
int after = 0;
if (know == NULL)
{
eprintf ("Empty knowledge.");
2004-04-23 11:58:43 +01:00
return;
}
tl = knowledgeGetInverses (know);
if (tl == NULL)
{
eprintf ("None.");
2004-04-23 11:58:43 +01:00
}
else
{
while (tl != NULL && tl->next != NULL)
{
if (after)
{
eprintf (",");
2004-04-23 11:58:43 +01:00
}
eprintf ("(");
2004-04-23 11:58:43 +01:00
termPrint (tl->term);
eprintf (",");
2004-04-23 11:58:43 +01:00
termPrint (tl->next->term);
eprintf (")");
2004-04-23 11:58:43 +01:00
after = 1;
tl = tl->next->next;
}
}
}
2004-05-15 15:22:44 +01:00
//! Yield the set of representatives for the knowledge.
/**
* Note: this is a shallow copy, and needs to be termlistDelete'd.
*\sa termlistDelete()
2004-04-23 11:58:43 +01:00
*/
Termlist
2004-07-20 10:07:43 +01:00
knowledgeSet (const Knowledge know)
2004-04-23 11:58:43 +01:00
{
Termlist tl1, tl2;
tl1 = termlistShallow (know->basic);
tl2 = termlistShallow (know->encrypt);
return termlistConcat (tl1, tl2);
}
2004-05-15 15:22:44 +01:00
//! Get the inverses pointer of the knowledge.
/**
* Essentially the inverse function of knowledgeSetInverses()
*/
2004-04-23 11:58:43 +01:00
Termlist
2004-07-20 10:07:43 +01:00
knowledgeGetInverses (const Knowledge know)
2004-04-23 11:58:43 +01:00
{
if (know == NULL)
return NULL;
else
return know->inverses;
}
2004-07-20 10:07:43 +01:00
//! Get all basic elements in the knowledge
/**
* This function is used by match_basic, to determine all basic elements in the knowledge set.
* Most of the time this doesn't even change, so it might become a parameter of knowledge.
* For now, this will have to do.
*
*@todo Investigate whether the basics in the knowledge set should be a parameter of knowledge, as it doesn't change very often.
*/
__inline__ Termlist
knowledgeGetBasics (const Knowledge know)
{
return termlistAddBasics (termlistAddBasics (NULL, know->basic),
know->encrypt);
2004-07-20 10:07:43 +01:00
}
2004-05-15 15:22:44 +01:00
//! check whether any substitutions where made in a knowledge set.
/**
* Typically, when a substitution is made, a knowledge set has to be reconstructed.
* This procedure detects this by checking knowledge::vars.
*@return True iff an open variable was later closed by a substitution.
*\sa knowledgeReconstruction()
2004-04-23 11:58:43 +01:00
*/
int
knowledgeSubstNeeded (const Knowledge know)
{
Termlist tl;
if (know == NULL)
return 0;
tl = know->vars;
while (tl != NULL)
{
if (tl->term->subst != NULL)
return 1;
tl = tl->next;
}
return 0;
}
2004-05-15 15:22:44 +01:00
//! Reconstruct a knowledge set.
/**
2004-04-23 11:58:43 +01:00
* This is useful after e.g. substitutions.
* Just rebuilds the knowledge in a new (shallow) copy.
2004-05-15 15:22:44 +01:00
*@return The pointer to the new knowledge.
*\sa knowledgeSubstNeeded()
2004-04-23 11:58:43 +01:00
*/
Knowledge
knowledgeReconstruction (const Knowledge know)
{
Knowledge newknow = emptyKnowledge ();
newknow->inverses = know->inverses;
knowledgeAddTermlist (newknow, know->basic);
knowledgeAddTermlist (newknow, know->encrypt);
return newknow;
}
2004-05-15 15:22:44 +01:00
//! Propagate any substitutions just made.
/**
2004-04-23 11:58:43 +01:00
* This usually involves reconstruction of the complete knowledge, which is
* 'cheaper' than a thorough analysis, so we always make a copy.
2004-05-15 15:22:44 +01:00
*\sa knowledgeReconstruction()
2004-04-23 11:58:43 +01:00
*/
Knowledge
knowledgeSubstDo (const Knowledge know)
{
/* otherwise a copy (for deletion) is returned. */
return knowledgeReconstruction (know);
}
2004-05-15 15:22:44 +01:00
//! Undo substitutions that were not propagated yet.
/**
* Undo the substitutions just made. Note that this does not work anymore after knowledgeSubstDo()
2004-04-23 11:58:43 +01:00
*/
void
knowledgeSubstUndo (const Knowledge know)
{
Termlist tl;
tl = know->vars;
while (tl != NULL)
{
tl->term->subst = NULL;
tl = tl->next;
}
}
2004-05-15 15:22:44 +01:00
//! Yield the minimal set of terms that are in some knowledge, but not in some other set.
/**
* Yield a termlist (or NULL) that represents the reduced items that are
2004-04-23 11:58:43 +01:00
* in the new set, but not in the old one.
2004-05-15 15:22:44 +01:00
*@param oldk The old knowledge.
*@param newk The new knowledge, possibly with new terms.
*@return A termlist of miminal terms in newk, but not in oldk.
2004-04-23 11:58:43 +01:00
*/
Termlist
knowledgeNew (const Knowledge oldk, const Knowledge newk)
{
Termlist newtl;
void addNewStuff (Termlist tl)
{
while (tl != NULL)
{
if (!inKnowledge (oldk, tl->term))
{
newtl = termlistAdd (newtl, tl->term);
}
tl = tl->next;
}
}
2004-05-26 13:17:09 +01:00
newtl = NULL;
2004-04-23 11:58:43 +01:00
addNewStuff (newk->basic);
addNewStuff (newk->encrypt);
return newtl;
}