/* -*- C++ -*- * mu_util.h * @(#) header for Auxiliary routines for the driver for Murphi verifiers. * * Copyright (C) 1992 - 1999 by the Board of Trustees of * Leland Stanford Junior University. * * License to use, copy, modify, sell and/or distribute this software * and its documentation any purpose is hereby granted without royalty, * subject to the following terms and conditions: * * 1. The above copyright notice and this permission notice must * appear in all copies of the software and related documentation. * * 2. The name of Stanford University may not be used in advertising or * publicity pertaining to distribution of the software without the * specific, prior written permission of Stanford. * * 3. This software may not be called "Murphi" if it has been modified * in any way, without the specific prior written permission of David L. * Dill. * * 4. THE SOFTWARE IS PROVIDED "AS-IS" AND STANFORD MAKES NO * REPRESENTATIONS OR WARRANTIES, EXPRESS OR IMPLIED, BY WAY OF EXAMPLE, * BUT NOT LIMITATION. STANFORD MAKES NO REPRESENTATIONS OR WARRANTIES * OF MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR PURPOSE OR THAT THE * USE OF THE SOFTWARE WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS * TRADEMARKS OR OTHER RIGHTS. STANFORD SHALL NOT BE LIABLE FOR ANY * LIABILITY OR DAMAGES WITH RESPECT TO ANY CLAIM BY LICENSEE OR ANY * THIRD PARTY ON ACCOUNT OF, OR ARISING FROM THE LICENSE, OR ANY * SUBLICENSE OR USE OF THE SOFTWARE OR ANY SERVICE OR SUPPORT. * * LICENSEE shall indemnify, hold harmless and defend STANFORD and its * trustees, officers, employees, students and agents against any and all * claims arising out of the exercise of any rights under this Agreement, * including, without limiting the generality of the foregoing, against * any damages, losses or liabilities whatsoever with respect to death or * injury to person or damage to property arising from or out of the * possession, use, or operation of Software or Licensed Program(s) by * LICENSEE or its customers. * * Read the file "license" distributed with these sources, or call * Murphi with the -l switch for additional information. * */ /* * Original Author: Ralph Melton * Extracted from mu_epilog.inc and mu_prolog.inc * by C. Norris Ip * Created: 21 April 93 * * Update: * */ #include // if you change this, // please make sure that you change a lot of other things // including array index error checking #ifndef ALIGN // Norris: Must be zero #define UNDEFVAL 0 #define UNDEFVALLONG 0 #else // Norris: the biggest value storable #define UNDEFVAL 0xff #define UNDEFVALLONG INT_MIN #endif /**************************************** There are 4 groups of declarations: 1) utility functions (not in any class) 2) mu__int / mu__boolean 3) world_class 4) timer (not in any class) 5) random number generator ****************************************/ /**************************************** Utility functions ****************************************/ const char* StrStr(const char* super, const char* sub ); void ErrAlloc( void *p ); void err_new_handler(void); // Uli: CATCH_DIV has to be defined or undefined depending on compiler // and operating system (see Makefile) #ifndef CATCH_DIV void catch_div_by_zero(...); // for most compilers #else void catch_div_by_zero(int); // for CC on elaines #endif bool IsPrime( unsigned long n ); unsigned long NextPrime( unsigned long n ); unsigned long NumStatesGivenBytes( unsigned long bytes ); char *tsprintf (char *fmt, ...); /**************************************** The base class for a value ****************************************/ // Uli: general comments about the variables: // - they are local by default // - they are made global by calling to_state() class mu__int /* a base for a value. */ { enum { undef_value=UNDEFVAL }; // Uli: nice way to declare constants void operator=(mu__int&); // Uli: disallow copying, this can catch // possible errors in the Murphi // compiler protected: bool in_world; // if TRUE global variable, otherwise local int lb, ub; // lower bound and upper bound int offset, size; // offset in the state vector, size (both in bits) #ifndef ALIGN position where; // more info on position in state vector #else int byteOffset; // offset in state vector in bytes unsigned char *valptr; // points either into state vector (for globals) // or to data member cvalue #endif bool initialized; // whether it is initialized in the startstate // Uli: seems not to be used any more unsigned char cvalue; // contains value of local variable public: char *name; // name of the variable char longname[BUFFER_SIZE / 4]; // - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - // constructors mu__int(int lb, int ub, int size, char *n, int os ) :lb(lb), ub(ub), size(size), initialized(FALSE) { set_self(n, os); undefined(); }; mu__int(int lb, int ub, int size) :lb(lb), ub(ub), size(size), initialized(FALSE) { set_self(NULL,0); undefined(); }; // Uli: - seems not to be used any more // - however, I left it here since it does the correct things mu__int(int lb, int ub, int size, int val) :lb(lb), ub(ub), size(size) { set_self("Parameter or function result", 0); operator=(val); }; // Uli: this constructor is called implicitly for function results // by the code generated by the Murphi compiler mu__int(const mu__int &src) :lb(src.lb), ub(src.ub), size(src.size), in_world(FALSE) { set_self("Function result", 0); value(src.value()); // value() allows returning undefined values }; // a destructor. virtual ~mu__int( void ) { }; // routines for constructor use void set_self_ar( char *n1, char *n2, int os ) { // sets the name int l1 = strlen(n1), l2 = strlen(n2); // without using strcpy( longname, n1 ); // tsprintf longname[l1] = '['; strcpy( longname+l1+1, n2 ); longname[l1+l2+1] = ']'; longname[l1+l2+2] = 0; set_self( longname, os ); }; void set_self_2( char *n1, char *n2, int os ) { // sets the name strcpy( longname, n1 ); // without using strcat( longname, n2 ); // tsprintf set_self( longname, os ); }; void set_self( char *n, int os ) { name = n; offset = os; in_world = FALSE; // Uli: variables are local by default #ifdef ALIGN byteOffset = offset/8; valptr = (unsigned char *)&cvalue; #else where.longoffset = os / 32; if (size < 0) { where.mask1 = 0; where.shift1 = 0; where.mask2 = 0; where.shift2 = 0; } else { where.shift1 = os % 32; where.mask1 = (1<= lb ) ) { value(val); initialized = TRUE; } else boundary_error(val); return val; } #else int operator= (int val) { return value(val); } #endif // conversion to int #ifndef NO_RUN_TIME_CHECKING int undef_error() const; inline operator int() const { if (isundefined()) return undef_error(); return value(); }; #else inline operator int() const { return value(); }; #endif // new data access routines // Uli: - the number of functions defined here could be reduced // - new names would be good as well // ("undefine" instead of "undefined", etc.) #ifdef ALIGN inline const int value() const { return *valptr; }; inline int value(int val) { *valptr = val; return val; }; inline void defined(bool val) { if (!val) *valptr = undef_value; }; inline bool defined() const { return (*valptr != undef_value); }; inline void undefined() { *valptr = undef_value; }; inline bool isundefined() const { return (*valptr == undef_value); }; #else inline const int value() const { if (in_world) return workingstate->get(&where)+lb-1; else return cvalue+lb-1; }; inline int value(int val) { if (in_world) workingstate->set(&where, val - lb + 1); else cvalue = val - lb +1; return val; }; inline void defined(bool val) { if (!val) if (in_world) workingstate->set(&where,undef_value); else cvalue = undef_value; }; inline bool defined() const { if (in_world) return (workingstate->get(&where) != undef_value); else return cvalue != undef_value; }; inline void undefined() { defined(FALSE); }; inline bool isundefined() const { if (in_world) return (workingstate->get(&where) == undef_value); else return cvalue == undef_value; }; #endif // - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - // printing, etc. // printing routines virtual void print() { if (defined()) cout << name << ":" << value() << '\n'; else cout << name << ":Undefined\n" ; }; friend ostream& operator<< (ostream& s, mu__int& val) { if (val.defined()) s << val.value(); else s << "Undefined"; return s; // changed by Uli } void print_diff(state *prevstate); // transfer routines void to_state(state *thestate) { int val = value(); // Uli: copy value (which is probably undefined) in_world = TRUE; #ifdef ALIGN valptr = (unsigned char *)&(workingstate->bits[byteOffset]); #endif value(val); }; void from_state(state *thestate) { }; // - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - // comparing routines, for symmetry friend int CompareWeight(mu__int& a, mu__int& b) { if (!a.defined() && !b.defined()) return 0; else if (!a.defined()) return -1; else if (!b.defined()) return 1; else if (a.value()==b.value()) return 0; else if (a.value()>b.value()) return 1; else return -1; }; friend int Compare(mu__int& a, mu__int& b) { if (!a.defined() && !b.defined()) return 0; else if (!a.defined()) return -1; else if (!b.defined()) return 1; else if (a.value()==b.value()) return 0; else if (a.value()>b.value()) return 1; else return -1; }; virtual void MultisetSort() {}; }; /**************************************** The class for a short int (byte) ****************************************/ class mu__byte: public mu__int { public: // constructors mu__byte(int lb, int ub, int size, char *n, int os ) : mu__int(lb,ub,size,n,os) {}; mu__byte(int lb, int ub, int size) : mu__int(lb,ub,size) {}; mu__byte(int lb, int ub, int size, int val) : mu__int(lb,ub,size,val) {}; // assignment int operator= (int val) { return mu__int::operator=(val); } }; /**************************************** The class for a long int ****************************************/ // Uli: - this class redefines most almost all functions to access the // data // - this is necessary because of the different layout of the data // - templates may provide a more elegant solution // however: pointer-access to the values in the state vector is // not possible since they are not individually aligned class mu__long: public mu__int { enum { undef_value=UNDEFVALLONG }; public: int cvalue; // Uli: hides the cvalue from the base class mu__int // - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - // constructors // Uli: example problem with the constructors: // - the undefined() in the mu__int constructor does not set the mu__long // cvalue // - the programming is not too nice, improving, however, seems to require // lots of changes in the code mu__long(int lb, int ub, int size, char *n, int os ) :mu__int(lb,ub,size,n,os) { undefined(); }; mu__long(int lb, int ub, int size) :mu__int(lb,ub,size) { undefined(); }; mu__long(int lb, int ub, int size, int val) :mu__int(lb,ub,size,val) { operator=(val); }; mu__long(const mu__long &src) :mu__int(src) { value(src.value()); }; // - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - // data access routines inline void clear() { value(lb); initialized = TRUE; }; inline void undefine() { undefined(); initialized = TRUE; }; inline void reset() { undefined(); initialized = FALSE; }; // assignment #ifndef NO_RUN_TIME_CHECKING int operator= (int val) { if ( ( val <= ub ) && ( val >= lb ) ) { value(val); initialized = TRUE; } else boundary_error(val); return val; } #else int operator= (int val) { return value(val); } #endif // conversion to int #ifndef NO_RUN_TIME_CHECKING inline operator int() const { if (isundefined()) return undef_error(); return value(); }; #else inline operator int() const { return value(); }; #endif // new data access routines #ifdef ALIGN inline const int value() const { if (in_world) return workingstate->getlong(byteOffset); else return cvalue; }; inline int value(int val) { if (in_world) workingstate->setlong(byteOffset, val); else cvalue = val; return val; }; inline void undefined() { if (!in_world) cvalue = undef_value; else workingstate->setlong(byteOffset,undef_value); }; inline void defined(bool val) { if (!val) if (!in_world) cvalue = undef_value; else workingstate->setlong(byteOffset,undef_value); }; bool defined() const { if (in_world) return (workingstate->getlong(byteOffset) != undef_value); else return cvalue != undef_value; }; bool isundefined() const { if (in_world) return (workingstate->getlong(byteOffset) == undef_value); else return cvalue == undef_value; }; #else // Uli: - code from mu__int has to be duplicated here // - otherwise the wrong cvalue/undef_value is accessed inline const int value() const { if (in_world) return workingstate->get(&where)+lb-1; else return cvalue+lb-1; }; inline int value(int val) { if (in_world) workingstate->set(&where, val - lb + 1); else cvalue = val - lb +1; return val; }; inline void defined(bool val) { if (!val) if (in_world) workingstate->set(&where,undef_value); else cvalue = undef_value; }; inline bool defined() const { if (in_world) return (workingstate->get(&where) != undef_value); else return cvalue != undef_value; }; inline void undefined() { defined(FALSE); }; inline bool isundefined() const { if (in_world) return (workingstate->get(&where) == undef_value); else return cvalue == undef_value; }; #endif // - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - // printing, etc. // printing routine, added by Uli virtual void print() { if (defined()) cout << name << ":" << value() << '\n'; else cout << name << ":Undefined\n"; } friend ostream& operator<< (ostream& s, mu__long& val) { if (val.defined()) s << (int)val; else s << "Undefined" ; return s; } void print_diff(state *prev); // transfer routines void to_state(state *thestate) { int val = value(); // Uli: copy value (which is probably undefined) in_world = TRUE; value(val); }; // - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - // comparing routines, for symmetry friend int CompareWeight(mu__long& a, mu__long& b) { if (!a.defined() && !b.defined()) return 0; else if (!a.defined()) return -1; else if (!b.defined()) return 1; else if (a.value()==b.value()) return 0; else if (a.value()>b.value()) return 1; else return -1; }; friend int Compare(mu__long& a, mu__long& b) { if (!a.defined() && !b.defined()) return 0; else if (!a.defined()) return -1; else if (!b.defined()) return 1; else if (a.value()==b.value()) return 0; else if (a.value()>b.value()) return 1; else return -1; }; }; /**************************************** The class for a boolean ****************************************/ class mu_0_boolean: public mu__int /* In the Murphi compilation, we typecheck against mixing ints and enums, * so now, we can allow it to be mixed with integers without catastrophe. */ { // extra data from mu__int static char * values[]; // special stream operation --> use names false or true friend ostream& operator<<(ostream& s, mu_0_boolean& x) { if (x.defined()) return s << mu_0_boolean::values[int(x)]; else return s << "Undefined" ; } public: #ifndef NO_RUN_TIME_CHECKING inline int operator=(int val) { initialized = TRUE; return value(val ? 1 : 0); }; inline int operator= (const mu_0_boolean& val ) { initialized = TRUE; return value(val ? 1 : 0); }; #else inline int operator=(int val) { return value(val); }; inline int operator= (const mu_0_boolean& val ) { return value(val); }; #endif mu_0_boolean (char *name, int os) : mu__int(0,1,2, name, os) {}; mu_0_boolean ( void) : mu__int(0,1,2) {}; mu_0_boolean (int val ) : mu__int(0,1,2, "Parameter or function result", 0) { operator=(val); }; // special assignment for boolean char * Name() { return values[value()]; }; // canonicalization function for symmetry virtual void Permute(PermSet& Perm, int i); virtual void SimpleCanonicalize(PermSet& Perm); virtual void Canonicalize(PermSet& Perm); virtual void SimpleLimit(PermSet& Perm); virtual void ArrayLimit(PermSet& Perm); virtual void Limit(PermSet& Perm); // special print for boolean --> use name False or True virtual void print() { if (defined()) cout << name << ":" << values[value()] << '\n'; else cout << name << ":Undefined\n"; }; void print_statistic() {}; }; /**************************************** world_class declarations ****************************************/ class world_class { public: void print(); /* print out the values of all variables. */ void print_statistic(); void print_diff( state *prevstate ); void clear(); /* clear every variable. */ void undefine(); /* undefine every variable. */ void reset(); /* uninitialize every variable. */ /* * this is something of a different approach than previous versions-- * we let the translation of the world * into states be a property of the world, * instead of a property of the state. */ void to_state(state *newstate); /* encode the world into newstate. */ state *getstate(); /* return a state encoding the values of all variables. */ state_L *getstate_L(); /* return a state_L */ void setstate( state *thestate ); /*set the state of the world to /*thestate.*/ }; /*************************** Timer ***************************/ double SecondsSinceStart( void ); /*************************** // added by Uli random number generator ***************************/ class randomGen // random number generator { private: unsigned long value; public: randomGen(); unsigned long next(); // return next random number }; /**************************************** 1) 20 Dec 93 Norris Ip: added the following to mu_0_boolean: void mu_0_boolean::Permute(PermSet& Perm, int i) {}; void mu_0_boolean::Canonicalize(PermSet& Perm) {}; void mu_0_boolean::Limit(PermSet& Perm) {}; 2) 28 Feb 94 Norris Ip: added the following to mu_0_boolean: void mu_0_boolean::SimpleCanonicalize(PermSet& Perm) {}; 3) 28 Feb 94 Norris Ip: fixed checking whether variable is initialized. 4) 8 March 94 Norris Ip: merge with the latest rel2.6 ****************************************/ /******************** $Log: mu_util.h,v $ Revision 1.2 1999/01/29 07:49:11 uli bugfixes Revision 1.4 1996/08/07 18:54:33 ip last bug fix on NextRule/SetNextEnabledRule has a bug; fixed this turn Revision 1.3 1996/08/07 01:00:18 ip Fixed bug on what_rule setting during guard evaluation; otherwise, bad diagnoistic message on undefine error on guard Revision 1.2 1996/08/07 00:15:26 ip fixed while code generation bug Revision 1.1 1996/08/07 00:14:46 ip Initial revision ********************/