Open Collections

UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Source-level transformations for improved formal verification Winters, Brian D. 2000

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Item Metadata

Download

Media
831-ubc_2000-0612.pdf [ 4.5MB ]
Metadata
JSON: 831-1.0051531.json
JSON-LD: 831-1.0051531-ld.json
RDF/XML (Pretty): 831-1.0051531-rdf.xml
RDF/JSON: 831-1.0051531-rdf.json
Turtle: 831-1.0051531-turtle.txt
N-Triples: 831-1.0051531-rdf-ntriples.txt
Original Record: 831-1.0051531-source.json
Full Text
831-1.0051531-fulltext.txt
Citation
831-1.0051531.ris

Full Text

S o u r c e - L e v e l T r a n s f o r m a t i o n s for I m p r o v e d F o r m a l V e r i f i c a t i o n by Brian D. Winters B.S., California Institute of Technology, 1997 A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF Master of Science in THE FACULTY OF GRADUATE STUDIES (Department of Computer Science) we accept this thesis as conforming to the required standard T h e U n i v e r s i t y o f B r i t i s h C o l u m b i a August 2000 © Brian D. Winters, 2000 In p r e s e n t i n g t h i s t h e s i s i n p a r t i a l f u l f i l m e n t of the requirements f o r an advanced degree at the U n i v e r s i t y of B r i t i s h Columbia, I agree that the L i b r a r y s h a l l make i t f r e e l y a v a i l a b l e f o r reference and study. I f u r t h e r agree that permission f o r extensive copying of t h i s t h e s i s f o r s c h o l a r l y purposes may be granted by the head of my department or by h i s or her r e p r e s e n t a t i v e s . I t i s understood that copying or p u b l i c a t i o n of t h i s t h e s i s f o r f i n a n c i a l g a i n s h a l l not be allowed without my w r i t t e n permission. Department of rv\ p u The U n i v e r s i t y of B r i t i s h Columbia Vancouver, Canada Abstract A major obstacle to widespread acceptance of formal verification is the difficulty in using the tools effectively. Although learning the basic syntax and operation of a formal verification tool may be easy, expert users are often able to accomplish a verification task while a novice user encounters time-out or space-out attempting the same task. In this thesis, we assert that often a novice user will model a system in a different manner — semantically equivalent, but less efficient for the verification tool — than an expert user would, that some of these inefficient modeling choices can be easily detected at the source-code level, and that a robust verification tool should identify these inefficiencies and optimize them, thereby helping to close the gap between novice and expert users. To test our hypothesis, we propose some possible optimizations for the Mur<£> verification system, implement one of these, and compare the results on a variety of examples written by both experts and novices (the Mury? distribution examples, a set of cache coherence protocol models, and a portion of the IEEE 1394 Firewire protocol). The results support our assertion — a nontrivial fraction of the Mur</? models written by novice users were significantly accelerated by the single optimization. Our findings strongly support further research in this area. Contents Abstract ii Contents iii List of Tables vi List of Figures vii Acknowledgments viii Dedication ix 1 Introduction 1 1.1 Motivation 1 1.2 Project 3 1.3 Contribution 4 2 Background 5 2.1 Mury 5 2.2 Related Work 10 iii 3 Source-Level Transformations 12 3.1 Ruleset Rearrangement 12 3.2 Scalarset Identification 15 3.3 Variable Clearing 16 4 Implementation 18 4.1 Mury? 3.1 19 4.2 Murf Optimizer 19 4.3 Suggestions for Future Attempts 21 5 Experiments 23 5.1 Methodology : 23 5.2 Results 24 6 Conclusions and Future Work 35 Bibliography 38 Appendix A Mur</? Optimizer Source 41 A.l C++ Header Files 42 A. 1.1 mu.opt.h 42 A.1.2 mu_opt_base.h 42 A. 1.3 mu_opt_decl.h 43 A. 1.4 mu_opt_expr.h 45 A. 1.5 mu-opt_param.h 47 A.1.6 mu_opt-root.h 48 A.1.7 mu.opt_rule.h 49 A.1.8 mu_opt-ste.h 52 iv A. 1.9 mu_opt_stmt.h 53 A.1.10 mu_opt_typedecl.h 58 A.2 C++ Program Files 61 A.2.1 mu_opt_base.cc 61 A.2.2 mu_opt_decl.cc 61 A.2.3 mu_opt_expr.cc 69 A.2.4 mu_opt_param.cc 72 A.2.5 mu_opt_root.ee 76 A.2.6 mu_opt_rule.cc 78 A.2.7 mu_opt_ste.ee 93 A.2.8 mu_opt_stmt.ee 96 A. 2.9 mu_opt_typedecl.cc I l l A. 3 Other Files 118 A.3.1 Murphi3.1-muopt.patch 118 A.3.2 Makefile 121 Appendix B Firewire Model Source 123 B. l Novice Firewire Model 123 B.2 Later Firewire Model 137 v List of Tables 5.1 Murf example verification times, without hash compaction 25 5.2 Mury example verification times, with hash compaction 26 5.3 Cache coherence protocol verification times, without hash compaction 27 5.4 Cache coherence protocol verification times, with hash compaction . 27 5.5 Verification times for partial model of IEEE 1394, without hash compaction 30 5.6 Verification times for partial model of IEEE 1394, with hash compaction 30 5.7 Mm<p example compilation times, without hash compaction 31 5.8 Mury example compilation times, with hash compaction 32 5.9 Cache coherence protocol compilation times, without hash compaction 33 5.10 Cache coherence protocol compilation times, with hash compaction . 33 5.11 Compilation times for partial model of IEEE 1394, without hash compaction 34 5.12 Compilation times for partial model of IEEE 1394, with hash compaction 34 vi List of Figures 2.1 Fragments from a Mur<£ Model of a Cache Coherence Protocol . . . 8 2.2 An example of ungrouping two rules from Figure 2.1 9 3.1 The result of applying ruleset rearrangement to the example in Figure 2.1 14 vn Acknowledgments This work would not have been possible without extensive support and encourage-ment from Alan Hu. I owe many individuals a debt of gratitude for helping me to find this path, and for making the journey more enjoyable. Most important of these were Wendy Belluomini, who provided invaluable advice and guidance, and H. Peter Hofstee, who taught me many valuable lessons and was always generous in his support. Lastly, I might have missed the boat completely, had Tom Zavisca not twisted my arm at the right time. B R I A N D . W I N T E R S The University of British Columbia August 2000 vm To my parents, for their endless patience and support. ix Chapter 1 Introduction A major obstacle to widespread acceptance of formal verification is the difficulty in using the tools effectively. Ideally, the tools should be accessible to non-experts, so that formal verification can be used as just another technique to aid design and verification. While some effort learning a tool can be expected, the user must not be expected to have a deep understanding of the specific algorithms and heuristics used by the tool. In reality, the situation is markedly different. Although the syntax and basic operation of formal verification tools might be easy to learn, there is usually considerable subtlety in using the tools effectively on large problems. Expert users with a deep understanding of a tool are able to achieve impressive results; novice users are all too frequently frustrated by exploding memory and C P U time usage. 1.1 Motivation A key difference between novice and expert is that the expert has a detailed under-standing of the algorithms and heuristics used by a tool and can use that under-standing to choose an efficient way to present the verification problem to the tool. 1 When applying formal verification, many choices must be made: how to model parts of the system, which parts of a system to abstract, how to perform that abstraction, and so forth. Differing choices can result in an equivalent verification problem, but some choices will be more or less efficient than others for the particular verification tool. When the novice has the chance to consult with the expert, advice often takes the form, "Don't model it like that; do this instead. Otherwise, . . . ," where the consequence reflects detailed knowledge of the tool: the BDD will have to represent all permutations, the state space will lose symmetry, the reduction heuristic will not work, and so forth. This situation is clearly undesirable; the novice is forced to be-come an expert on and adapt to the idiosyncrasies of the tool. Even for the expert, being forced to adapt to the tool can be suboptinial, since the description style that most clearly matches the verification problem might not be the style that best suits the verification tool. Also, over time the algorithms used by the tool may change, forcing the expert to rewrite models in order to take advantage of improvements to the tool. Rather than forcing the user to adapt to the tool, the tool should adapt to the user. A robust, practical verification tool should help close the gap between novice and expert, allowing the novice to get useful results without a lengthy learning curve. For novice and expert alike, the tool should free the user to match the description to the problem being verified, rather than to specific quirks of the verification tool. We hypothesize that often a novice will model a system differently (less efficiently for the tool) than an expert would, that many of these inefficient modeling choices can be easily detected in the source code of the model description, and that the tool should be able to optimize away these differences. 2 1.2 Project To test our hypothesis, we consider a small set of source-level transformations with a specific tool. We have chosen the Mury? verification system [6, 5] as the target for our test. The choice of Mury is fairly arbitrary — our ideas should apply in general, although specific optimizations, obviously, apply only to verification tools with similar features. We will give a brief overview of Mury? in Chapter 2, followed by a sampling of related work. In Chapter 3, we will propose three possible Mury? source-level transforma-tions which may improve models written by novice users. The first, ruleset re-arrangement, eliminates redundant rule firings. These extra rule firings can occur when users group rules without considering the implementation details of how Mury> evaluates rules. The second, scalarset identification, is an automatic means of find-ing a particular type of symmetry. Exploiting symmetry can significantly reduce both time and space requirements, but novices may not understand how symmetry works or the importance of exploiting it. The last transformation, variable clearing, evaluates data dependencies to find when variables are no longer relevant. Failing to clear variables when they become irrelevant causes creation of redundant states, increasing time and space requirements. As with the other transformations, novices are unlikely to grasp the impact of variable clearing on the verification of their model. We have implemented the first proposed transformation, ruleset rearrange-ment, as a modification of Mury> 3.1. We chose not to implement scalarset identifi-cation and automatic variable clearing, because of structural problems in the Mury? compiler. In Chapter 4 we will describe our implementation and the details of those problems. 3 To test the effectiveness of our transformation, we apply it to three sets of examples, including models written by both experts and novices. The results of our experiments, which we will present in Chapter 5, support our hypothesis. Novice users do model problems differently, and some styles are less efficient for the tool than others. In many cases, the application of source-level transformations corrects those inefficiencies. 1.3 C o n t r i b u t i o n The primary contribution of our work is the identification of a new research area. To date, work on optimizing verification has focused on improving the fundamental algorithms. We assert that optimizations which close the gap between novice and expert are also important, and support our assertion with positive experimental re-sults. Furthermore, we identify several source-level transformations which can help to close this gap, and implement one. In the process of evaluating that transfor-mation, we have developed necessary infrastructure for performing optimizations in Mury? 3.1 and identified impediments to implementation of further source-level optimizations. Finally, we provide advice for follow-on research using the Murty? platform. 4 C h a p t e r 2 Background In this chapter we provide background on the Murf verifier, with details on the features which are relevant to our work, and an overview of related work. 2 . 1 Mur</> We have chosen the Muif verification system [6, 5] as the basis for our optimiza-tions. The Mm<p verifier is a model checker which performs explicit state space reachability.1 Mur</9 has been widely used for a variety of applications (e.g., [7, 25, 18, 10, 19, 11]). The Mury verifier has it's own input language for describing the system being verified. This Mmf language is a high-level, guarded-command language [4, 3]. A Mmip program consists of two main parts: declarations and rules. The declaration section is Pascal-like and declares constants, types, global variables, and procedures. The rules define the transitions of the system. At any given time, the system state is determined by the values of the global variables. As the system executes, a rule is 1For additional information see http://verify.stanford.edu/dill/murphi.html. 5 chosen nondeterministically and executes atomically, updating the global variables to a new state. Compiling a Mury model is a two step process. First Mury transforms the model into a C++ program which verifies the model. Then a C++ compiler is used to turn that program into an executable. Most elements of a Mury? model translate well into C++, with the exception of rule execution. Since Mury? is verifying the model for all possible executions, all rules are attempted for each visited state. Mury? tracks visited states in a table, which can become very large. Mury offers two options, bit compaction and hash compaction, to reduce the memory requirements of the state table. These options trade increased computation time for reduced space. Bit compaction packs states rather than word-aligning them, which may have a dramatic impact on the memory requirements of some models. Hash compaction does not store full state information in the state table, but rather stores a hash of the state. At the end of a run Mury> gives the probability of a hash collision on that run. The hash function is different for each run of a model, allowing multiple runs to be used to reduce the overall probability that states have been missed. Bit compaction and hash compaction may be combined. Mury? provides several features to simplify writing scalable descriptions of large systems. The normal description style uses numerous subrange types, which can be scaled easily. Of particular interest to this thesis are the special scalarset and multiset types, which provide automatic symmetry reduction [15]. Scalarsets are like subranges, but without order. Multisets are like arrays, except that the array elements are unordered. Appropriate use of these data types greatly reduces the size of the state space. To simplify writing rules for all values of a subrange or scalarset, Mury? provides a ruleset construct, which generates a copy of all enclosed 6 Const ProcCount: 2; — # of processors AddressCount: 2; — # of addresses ValueCount: 2; — # of distinct values Type Pid: Scalarset(ProcCount); Address: Scalarset(AddressCount); Value: Scalarset(ValueCount); ProcState: Record cache: Array[Address] of Record v: Value; End; End; Var procs: Array[Pid] of ProcState; Procedure flushCache(p: Pid); Begin End; (Figure 2.1, continued on next page) 7 (continuation of Figure 2.1) Ruleset p: Pid Do Alias me: procs [p] Do Ruleset a: Address Do Ruleset v: Value Do Rule "Evict shared data" (me.cache[a].state = Shared) ==> me.cache[a].state := Invalid; Undef ine me.cache[a].v; Endrule; Rule "Change exclusive copy" (me.cache[a].state = Exclusive) ==> me.cache[a].v := v; Endrule; Rule "Processor reset" true ==> flushCache(p); Endrule; Endruleset; Endruleset; Endalias; Endruleset; Figure 2.1: Fragments from a Mury Model of a Cache Coherence Protocol. The syntax is similar to Pascal, extended to support specifying rules as guarded com-mands. There are two main sections, for declarations (e.g., Const, Type, Var and Procedure) and for rules (e.g., Ruleset and Alias). The scalarset definitions are like subranges, except that they permit automatic symmetry reduction. In this ex-ample, the rulesets instantiate the rules for all possible processors, addresses, and values. The rules shown allow any processor to evict any address that it has cached in the shared state, any processor to change to any value any address that it has cached exclusive, and any processor to flush its cache. 8 Ruleset p: Pid Do Alias me: procs[p] Do Ruleset a: Address Do Ruleset v: Value Do Rule "Evict shared data" (me.cache[a].state = Shared) ==> me.cache[a].state := Invalid; Undefine me.cache[a].v; Endrule; Endruleset; Endruleset; Endalias; Endruleset; Ruleset p: Pid Do Alias me: procs [p] Do Ruleset a: Address Do Ruleset v: Value Do Rule "Change exclusive copy" (me.cache[a].state =,Exclusive) ==> me.cache[a].v := v; Endrule; Endruleset; Endruleset; Endalias; Endruleset; Figure 2.2: An example of ungrouping two rules from Figure 2.1. rules for each possible value of its formal parameter. Similarly, the choose construct selects an item from a multiset. Figure 2.1 shows some portions of a Mur</? model for a cache coherence protocol. Mury allows users to group rules within ruleset, choose, and alias statements, which can be nested arbitrarily. Grouping rules together under ruleset, choose or alias statements is logically equivalent2 to placing each rule under separate identical 2 In practice each ruleset, choose, and alias statement incurs a small amount of overhead, so grouping rules can improve performance very slightly. 9 ruleset, choose or alias statements, as in Figure 2.2. 2.2 Related W o r k The general concept of rewriting something to improve downstream performance is widespread, e.g., database query optimization or high-performance numerical code preprocessing, but this concept has not been applied to formal verification. Optimizing compilers perform source-level transformations, such as loop un-rolling, loop distribution, strength reduction, and induction variable removal [1, 20], some of which are similar to the Mury transformations we propose. Most program-ming languages are flexible, allowing the same idea to be expressed in many different ways. This flexibility empowers the user to express themselves in whatever way best suits their problem, rather than the way which best suits the compiler. One of the main goals of compiler optimization is to avoid penalizing users who do not express themselves in the way which directly translates to optimum performance. Mury takes advantage of compiler optimizations by generating C++ code which is then processed by an optimizing C++ compiler. The primary difference with our work is that compiler optimizations seek to optimize code execution speed, while we seek to improve the verification code which is to be compiled. Within the formal verification community, a great deal of research has gone into reducing memory usage and runtime (for examples, see some recent surveys [2, 8, 16, 9, 17]). These optimizations are written by experts for experts, optimizing the fundamental verification algorithms in ways that rarely can be expressed in the original language. Obviously, this research is complementary to ours; they optimize models written in a particular style, while we transform models written in a variety of styles into the particular styles which subsequently optimize well. The work most 10 closely related to ours is by Ip [14]. As with our work, he performs high-level analysis of Mury? programs during compilation to accelerate the verification, although again, his optimizations cannot be expressed in the source language, and therefore are not closing the gap between expert and novice. We have recently become aware of work by Yorav and Grumberg [26], which analyzes the control-flow graph of a Mury? program to reduce the size of the states-pace. They attempted two optimizations. One, which they call dead variable reduc-tion, reduces the statespace size by eliminating variables which are no longer used for computation. The optimization is very similar to our variable clearing trans-formation, described in Section 3.3. The other, called path reduction, shrinks the statespace by shortening computation paths, reducing the number of steps for each computation. 11 C h a p t e r 3 Source-Level Transformations In this chapter, we identify a few possible source-code transformations which may improve models written by novice users. These are ruleset rearrangement, scalarset identification, and variable clearing. 3.1 R u l e s e t R e a r r a n g e m e n t Mury allows users to group rules within ruleset, choose, and alias statements. These groupings are primarily for convenience; grouping of rules may be the best match for the problem semantics or may make it easier for the user to understand the model. If a rule is enclosed within a ruleset or choose statement on which it does not depend, the verifier will needlessly execute the rule for each possible value of the enclosing ruleset or choose parameter. The set of reachable states is unaffected, as each firing of that rule for variations of the independent variable will lead to the same state, but every extra rule firing adds to the runtime of the model. Obviously, rules should be moved outside the scope of irrelevant ruleset and 12 choose statements. Grouping of rules complicates removal. We will rely on two prop-erties to rewrite the description into an equivalent one that eliminates the needless rule firings: Notation Let a SimpleRule be any single rule statement. Let a Ruleset be any single ruleset, choose, or alias expression. Let a CompoundRule be any Simple-Rule, any Ruleset enclosing a CompoundRule, or any sequence o/CompoundRules. If <fi is a CompoundRule, let (</>) denote the CompoundRule formed by enclosing cf) in a Ruleset. Property 1 A CompoundRule 4> is equivalent to (4>) if <fi does not depend on the enclosing Ruleset. Property 2 Any Ruleset enclosing a sequence of CompoundRules (</>i, </>2,..., (j)n) is equivalent to {4>2), • • •, (4>n)-A straightforward implemention method starts by ungrouping all rules, so that each rule is alone within its enclosing ruleset, choose, and alias statements. Then, a check is performed to determine whether each rule is dependent on those enclosing statements. (Our ungrouping is similar to loop distribution [23], and our dependency check is similar to induction variable removal [24].) Independent ruleset and choose statements are removed, resulting in an equivalent model which executes faster. Independent alias removal does not directly impact performance, but it greatly simplifies the dependency analysis of parent ruleset and choose statements, so independent alias statements are also removed. For example, in Figure 2.1 the eviction rule does not depend on the ruleset over v, and the reset rule does not depend on t) or a. The transformation would convert the rules as shown in Figure 3.1. Each rule is now enclosed by only the relevant rulesets. 13 Ruleset p: Pid Do Alias me: procs[p] Do Ruleset a: Address Do Rule "Evict shared data" (me.cache[a].state = Shared) ==> me.cache[a].state := Invalid; Undefine me.cache[a].v; Endrule; Endruleset; Endalias; Endruleset; Ruleset p: Pid Do Alias me: procs [p] Do Ruleset a: Address Do Ruleset v: Value Do Rule "Change exclusive copy" (me.cache[a].state = Exclusive) ==> me.cache[a].v := v; Endrule; Endruleset; Endruleset; Endalias; Endruleset; Ruleset p: Pid Do Rule "Processor reset" true ==> flushCache(p); Endrule; Endruleset; Figure 3.1: The result of applying the ruleset rearrangement transformation to the example in Figure 2.1. Note that "Evict shared data" and "Processor reset" have fewer enclosing rulesets than in Figure 2.2, reducing the number of possible states which must be considered. 14 The idea of rearranging rulesets is not new, although ours is the first imple-mentation which produces optimal results in all cases. Mur<£> 3.1 employs an ad hoc heuristic which also attempts to skip some redundant iterations over independent variables. The heuristic shuffles a hierarchy of ruleset and choose statements, leav-ing rule groupings intact. The rule groupings obscure the dependency structure and defeat most optimizations. 3.2 Sca la r se t I d e n t i f i c a t i o n Using scalarsets instead of subranges in cases where ordering within the range does not matter provides a tremendous reduction in state space size. Subranges, how-ever, cannot always be replaced by scalarsets: any operation that relies on order, arithmetic, or distinguishing special elements in the range breaks symmetry and precludes the use of scalarsets. Novices might not realize all cases when a scalarset can be used. A triv-ial possible transformation is to check for each subrange type whether it could be redefined as a scalarset. A more interesting and powerful transformation is possible if one considers common programming practice. Data types are often reused for various purposes if it seems appropriate. An integer type, for example, might be used for a counter, for arithmetic, and for ID numbers. Returning to the example in Figure 2.1, suppose the user had defined an "integer" type as a subrange, and used this type for addresses, processor IDs, and values, as well as for some counters. In that model, one could not apply the scalarset symmetry reduction to addresses, processor IDs, and values, because the same type is also being used for counters, which have order. Even without the counters, having a single scalarset type for addresses, processor IDs, and 15 values would not allow as much symmetry reduction as having a separate scalarset for each. The data type reuse problem suggests a much more powerful solution to identify possible scalarsets. A syntactic check of the Murf program can determine which variables interact and must have the same type versus which variables have the same type simply for the user's convenience. A graph can be constructed with a node for each variable and edges indicating which variables must be type-compatible. Each connected component of the graph may be assigned a distinct type. Each of these types may then be checked separately for possible conversion to a scalarset. 3.3 Variable Clearing In most models, not all variables are holding important data at all times. For example, if a cache line is invalid, its contents do not matter, or if a queue is modeled as an array and a tail pointer, the array elements past the tail pointer do not matter. Although the contents of these variables may not matter to the user or to the accuracy of the model, they do matter to the verification tool. Two states that differ only in the values of don't-matter variables are still considered two distinct states by the verification tool. If the user is not careful to clear any leftover values out of variables whenever the the value no longer matters, the result is a needless explosion in the number of states. For example, in Figure 2.1, if the user omitted the Undef ine statement, the resulting model would have a much larger set of reachable states, because different values leftover in the me. cache [a] .v field would generate additional states. Tracking exactly which variables are no longer needed and making sure to 16 clear out their values is tedious for the expert user and extremely difficult for the novice, who may not even realize the importance of doing so. Fortunately, live variables analysis, a standard program analysis technique (e.g., [22]), can determine automatically which variables are dead (not needed) at each point in a program. Note that the Muif execution model, in which rules are chosen nondeterministically, results in a very conservative live variables analysis. Some limited data flow analysis to track rule enabling and disabling might strengthen the analysis considerably. Adapting live variables analysis to Mur</> programs could determine where Undef ine statements are needed. The source-code transformation would insert the Undef ine statements automatically, greatly improving the efficiency of verification. Recent work by Yorav and Grumberg [26] confirms that this is a promising area of research. 17 Chapter 4 Implementation This chapter discusses our implementation work. We begin with an overview of the relevant portions of Mury, followed by a detailed description of our optimizations. Finally, we will give advice for future optimization projects based on Mury. Since it was unlikely that our work would become part of the main Mury dis-tribution, we wished to avoid major changes to any specific version of the compiler. Mury's original design called for separate parsing and compilation stages, to allow additional processing stages, such as an optimizer, to be easily inserted between parsing and code generation. Our intent was to write routines which analyzed and then modified the parse tree, and to insert those routines between the parsing and code generation stages, saving us from having to develop our own code for parsing and output. Mury is a big language, and a full Mury parser would be complex and time consuming to produce. Unfortunately, the implementation of the current Mury compiler does not permit insertion of a meaningful optimization stage between the parser and the code generator. 18 4.1 M u r ^ 3.1 In this section we discuss the relevant details of the implementation of Murty? 3.1, the current version of the Mnvf compiler. There are numerous little details in Mur</> 3.1 that make implementing an optimization stage difficult, which are to be expected when modifying a mature program. The little details did not present significant obstacles. Unfortunately, the underlying structure of the Mury 3.1 compiler was an obstacle, and greatly hindered our efforts. Although at a high level it appears that Mury 3.1 still has separate parsing and compilation stages, a more detailed analysis of the source code shows that many aspects of the implementation violate the original object-oriented design. One aspect which proved nearly impossible to work around is that the parse tree is completely ignored after it is created. Code generation is performed using an independent set of data structures, which are generated at parse time along with the parse tree. Those data structures represent a partial compilation of the program. Our source-level transformations cannot be performed on the partially compiled program. Fortunately, the rule code generation data structure is simple enough that we can regenerate it after performing modifications on our parse tree. This allows us to perform ruleset rearrangement, but none of our other proposed transformations. 4.2 Mur<p O p t i m i z e r The ruleset rearrangement transformation is implemented as a modification of Murf 3.1. We added a small amount of helper code in one class, made neces-sary adjustments to protections on another class, added the appropriate calls to our code between parsing and code generation, and cleaned up a few problems with 19 ANSI C++ compliance. Appendix A.3.1 contains a full listing of the changes to Mury? 3.1, in unified cliff format. Our optimizer1 works in two stages. The first stage traverses Mury's parse tree, building a new version of that tree. The second stage traverses the new tree, performing any possible optimizations. The new parse tree is built to overcome deficiencies in the object-orientation of Mury? 3.1. All classes are derived from the same base class, and each class has consistent methods for dependency analysis and optimization. In proper object-oriented fashion, each class knows how to optimize itself. A typical optimize() method asks each child of the class to optimize, requests dependency information from those children, and then, based on its own state and the dependencies of its children, will perform transformations on itself. In some cases these transformations require creation of a replacement object based on a different class; such replacement objects are passed to the parent as the return value of optimize(). The ruleset rearrangement transformation requires dependency information from all children of the rule to know whether or not the rule is independent. For the most part, dependency analysis in a Mury> model should be easy. All of a model's state is contained in global variables, and most operations on those global variables are performed in rules, which are easy to analyze. The exception is when rules call functions or procedures. The simplest approach is to assume that all variables passed to a function or procedure are used in that function or procedure, but that may not always be the case. A more thorough approach would be to apply standard interprocedural data-flow analysis [21] to this problem. Unfortunately, it is very difficult to track variable dependencies in Mury 3.1. xFull source code for our optimizer may be found in Appendix A, or may be downloaded from h t t p : / / w w w . c s . u b c . c a / l a b s / i s d / P r o j e c t s / . 20 This is because Mury? 3.1 takes advantage of the subsequent C++ compilation step, maintaining as little information as possible about the details of the variable. In the absence of better information, our optimizer currently tracks dependencies by scope.2 Tracking dependencies by scope is sufficient for simple ruleset rearrange-ment, but is inadequate for tracing variable use through procedure and function calls. Ideally our optimizer should not be as large as it is. The extra size comes from recreating many of the structures present in the Mury? compiler. This redundancy is unfortunate, but was necessary given our design goals. 4.3 Sugges t i ons fo r F u t u r e A t t e m p t s Our current Mury? optimizer cannot be extended further without a major overhaul of Mury? 3.1. We believe that to be successful, any future work on source-level Mury? optimization should adopt one of two different approaches. One approach is to create a source-to-source optimizer. All of our proposed transformations are source-level, so an optimizer could ignore code generation en-tirely. We believe that because Mury? is a flexible language, many other desirable optimizations could also be performed at the source level. This approach requires writing a Mury? parser, but has the advantage that the program output is a trivial dump of the optimized parse tree. The other approach is to rewrite Mury. Such a rewrite should be based on completely separate parse, optimization, and compilation stages. The class structure of our Mury optimizer could be used as a basis for such a rewrite, but parse and compilation methods would need to be created, which is a nontrivial task. Without 2Each begin/end block in a Mury program constitutes a different scope. 21 borrowing substantial portions of Mur<^  3.1 compilation code, this approach also complicates any assertion that the resulting optimized model is equivalent to an unoptimized model produced through Murty? 3.1. 22 C h a p t e r 5 Experiments 5.1 Methodology Testing was performed on three sets of Mur<£> programs. The first set is the ex-amples included in the Mur</? distribution. These examples are written by expert Mur<£> users, so our hypothesis predicts little improvement from our optimization. The second set are eleven implementations of a simple, fictitious directory-based cache coherence protocol, each developed independently by students in a formal verification class. The students had no previous experience with Mur</?. They were given a tabular description of the cache coherence protocol and a partial Mur</2 model that included declarations, but no rules, so they were free to write the rules in whatever manner was most natural for them. This set of programs represents a large number of novice users independently tackling the same verification task. Our hypothesis predicts that some of these should benefit significantly from our optimization. The third experiment is a model of part of the physical layer of the IEEE 1394 [13] High Performance Serial Bus. The model implements the reset and 23 tree identification portions of the physical layer. The model is significantly larger than the others and was written by the author when he was a Mury novice. Large, real models written by novices are not widely available, but such models .provide the best test of our hypothesis because large real models written by novices are precisely those that we seek to improve. The Mury generated C++ code was compiled using egcs version 2.91.66 with " - 0 4 -mpent iumpro" optimization. The Mury hash table size was set to 96 MB with 30% for the active states. Experiments were run with and without hash compaction. With hash compaction, the default 40-bit hash size was used. The experiments were run on a 400 MHz Pentium II workstation with 128 MB of RAM, running SuSE Linux 6.1. 5.2 R e s u l t s The results of the experiments support our hypothesis. The size of the model (lines of code and number of states reached), runtime in seconds with and without op-timization, and percent improvement are reported for all models. The runtime reported is the median of five runs, in order to eliminate possible outlier effects.1 The results for the set of examples distributed with the Mury verifier are shown in Tables 5.1 and 5.2. As can be seen, the transformation had little effect on these programs, written by expert Mury users. This result is as expected by our hypothesis — the goal of our optimization is to improve the source code written by novice users, rather than trying to improve the fundamental verification algorithms. Worth noting, however, is that even this extremely simple transformation was able JFew outliers were observed, with most models showing less than 2% variation, fastest to slowest. Some of the smallest models (< Is running time) had variations as high as 20%, probably due to measurement error and operating system issues. 24 Model Lines States T i m 6 orig Timeopi % Imprv 2_peterson 135 13 2.51 2.51 0.00 abp 176 80 2.51 2.50 0.40 adash 2809 10466 20.99 21.18 -0.91 adashbug 2809 3742 6.66 6.69 -0.45 arbiter 114 502 1.91 1.91 0.00 cache3 1184 31433 9.73 9.78 -0.51 dek 135 100 2.50 2.50 0.00 down 87 10957 2.66 2.67 -0.38 dp4 151 112 2.49 2.49 0.00 dpnew 236 121 2.51 2.51 0.00 eadash 1880 133491 1453.73 1470.83 -1.18 ldash 1324 254986 1254.72 1162.85 7.32 lin 62 101 2.51 2.51 0.00 list6 333 23410 4.49 4.30 4.23 list6too 413 1077 4.57 4.59 -0.44 mcslockl 333 23644 5.63 5.63 0.00 mcslock2 390 540219 57.82 57.99 -0.29 n_peterson 203 163298 50.95 50.95 0.00 newcache3 1029 34781 53.11 53.20 -0.17 newlist6 309 13044 6.06 6.06 0.00 ns 449 467 1.25 1.28 -2.40 ns-old 449 17 1.23 1.23 0.00 pingpong 79 4 2.50 2.51 -0.40 sci 4875 18193 13.58 13.06 3.83 scierr 4875 64 1.24 1.24 0.00 sets 137 29 1.91 1.91 0.00 sort5 101 309 2.50 2.50 0.00 Table 5.1: Example programs distributed with the Mur<£> verifier, without hash compaction. Model name, number of lines of source code, number of reachable states, and unoptimized and optimized verification times in seconds are reported. Examples distributed with the Mur<^  verifier were written by experts. As expected by our hypothesis, they are mostly unaffected by our optimization. 25 Model Lines States Time0-t % Imprv 2_peterson 135 13 0.83 0.83 0.00 abp 176 80 0.84 0.84 0.00 adash 2809 10466 21.13 21.45 -1.51 adashbug 2809 3742 6.79 6.81 -0.29 arbiter 114 502 0.83 0.84 -1.20 cache3 1184 31433 10.22 10.26 -0.39 dek 135 100 0.82 0.82 0.00 down 87 10957 1.05 1.05 0.00 dp4 151 112 0.81 0.81 0.00 dpnew 236 121 0.84 0.84 0.00 eadash 1880 133491 1480.52 1479.43 0.07 ldash 1324 254986 1286.42 1179.33 8.32 lin 62 101 0.77 0.78 -1.30 list6 333 23410 4.60 4.56 0.87 list6too 413 1077 4.09 4.09 0.00 mcslockl 333 23644 5.28 5.28 0.00 mcslock2 390 540219 65.13 65.08 0.08 n_peterson 203 163298 53.48 53.43 0.09 newcache3 1029 34781 54.56 54.79 -0.42 newlist6 309 13044 5.94 5.93 0.17 ns 449 467 0.88 0.90 -2.27 ns-old 449 17 0.84 0.84 0.00 pingpong 79 4 0.83 0.84 -1.20 sci 4875 18193 13.54 13.71 -1.26 scierr 4875 64 0.82 0.82 0.00 sets 137 29 0.84 0.84 0.00 sort 5 101 309 0.82 0.83 -1.22 Table 5.2: Example programs distributed with the Mur<£ verifier, with hash com-paction. Examples distributed with the Mury verifier were written by experts. Again, these are mostly unaffected by our optimization. 26 Model Lines States Timeorj'g Timeo p i % Imprv student 1 587 1828 2.88 2.88 0.00 student2 641 36984 45.31 31.50 30.48 student3* 653 8204 4.38 4.39 -0.23 student4 710 501446 397.91 399.20 -0.32 student5 496 3522 3.17 3.17 0.00 student6 642 36995 44.21 30.94 30.02 student7 947 3647 3.52 3.48 1.14 student8 669 : 9071 6.87 6.83 0.58 student9* 714 52771 54.62 54.35 0.49 student 10 568 4403 3.97 .4.00 -0.76 student 11 538 1828 2.22 2.22 0.00 Table 5.3: Cache coherence protocol models, without hash compaction. On models written by novices, we expect that some will happen to be written in a manner that is not ideal for Mury. Those examples show significant improvement. All models were run with 2 processors, 3 addresses, 2 data values, and communication channels scaled as necessary, except those marked with an asterisk, which blew up with 3 addresses, so they were run with only 2 addresses. Model Lines States Time 0 Timeopt % Imprv student 1 587 1828 2.58 2.59 -0.39 student2 641 36984 46.28 32.48 29.82 student3* 653 8204 4.14 4.18 -0.97 student4 710 501446 417.02 416.93 0.02 student5 496 3522 2.92 2.92 0.00 student6 642 36995 44.96 31.94 28.96 student7 947 3647 3.32 3.23 2.71 student8 669 9071 6.80 6.78 0.29 student9* 714 52771 55.87 56.18 -0.55 studentlO 568 4403 3.81 3.82 -0.26 student 11 538 1828 1.95 1.96 -0.51 Table 5.4: Cache coherence protocol models, with hash compaction. Again, some examples written by novices show significant improvement. These models were run with the same parameters as in Table 5.3. 27 to give noticeable speedup on one model written by a Mury expert. Tables 5.3 and 5.4 show the results for the set of cache coherence protocol models, each developed independently by a different novice user. These models were tested with 2 processors, 3 addresses, and 2 data values. Communication channels were scaled to the minimum value which would allow verification of the model to complete. In this case, our hypothesis predicts that some of these programs should show significant improvement, corresponding to when a particular user chose a writing style that happens not to be well-suited to the internals of the tool. As expected, our simple optimization significantly speeds up two of the eleven programs. The enormous variations in code size, state count, and run times make it clear that different users naturally express themselves differently. A robust formal verification tool should adapt to this diversity, rather than forcing users to write code specifically tailored to the verification tool's idiosyncrasies. Results for the third test are shown in Tables 5.5 and 5.6. This program2 is a larger model of a real protocol, part of the IEEE 1394 "Firewire" standard. The program was written by a novice Mury user for whom the most natural way to model the system did not give the best arrangement of rules and rulesets for efficient Mury execution. The transformation significantly accelerated this example. It is again clear that novice users do not understand the subtleties of the verification tool, so their models might not be written in the most efficient manner for the tool. A simple source-code transformation helps rectify the problem. Compile times (Mury translation plus C++ compilation) for each model are shown in Tables 5.7, 5.8, 5.9, 5.10, 5.11, and 5.12. Times from only one compilation are reported, because the transformation does not significantly affect compile time. 2A listing of the model may be found in Appendix B.l. 28 In absolute terms, the worst compile time increase was 8.5 seconds on an example that required 255 seconds total. In percentage terms, the worst compile time increase was 18% on an example that required 10.2 seconds total. 29 Model Lines States TimeOR2(? Timeo p t % Imprv ieee-1394 824 2060216 372.23 271.43 27.08 Table 5.5: Partial model of the cable physical layer of the IEEE 1394 "Firewire" protocol, without hash compaction. Here we see results on a large example of a real system. The example was written by a novice Mury user and happened to be written in a style that the user found natural, but was not ideal for Mury. Our optimization improved performance considerably. Model Lines States Time^rip Timeo p i % Imprv ieee-1394 824 2060216 372.77 278.97 25.16 Table 5.6: Partial model of the cable physical layer of IEEE 1394, with hash com-paction. Again, our optimization improved performance considerably. 30 No Optimization With Optimization Model MurV time C++ time Mur</? time C++ time 2_peterson 0.04 12.22 0.05 12.36 abp 0.05 9.35 0.06 9.35 adash 0.17 112.63 3.27 112.71 adashbug 0.16 112.81 3.27 112.90 arbiter 0.04 10.38 0.05 10.59 cach3multi 0.02 0.02 0.02 0.02 cache3 0.08 53.07 0.51 53.02 dek 0.04 9.53 0.06 9.62 down 0.03 6.91 0.05 6.76 dp4 0.04 9.31 0.06 8.95 dpnew 0.04 11.04 0.07 11.05 eadash 0.13 95.37 1.55 95.65 ldash 0.09 75.90 1.21 75.57 lin 0.05 6.04 0.03 5.80 list6 0.06 20.48 0.12 20.30 list6too 0.08 29.91 0.28 29.74 mcslockl 0.06 19.36 0.07 19.36 mcslock2 0.06 27.58 0.09 27.53 n_peterson 0.04 15.37 0.05 15.42 newcache3 0.09 88.43 0.50 87.68 newlist6 0.06 37.11 0.08 37.12 ns 0.07 87.05 0.18 86.31 ns-old 0.06 86.51 0.18 86.28 pingpong 0.04 7.95 0.05 7.71 sci 0.57 244.83 7.18 246.64 scierr 0.78 241.44 7.72 240.82 sets 0.17 8.49 0.72 9.50 sort5 0.05 6.86 0.04 6.79 Table 5.7: Compilation times (in seconds) for example programs distributed with the Mm<p verifier, without hash compaction. 31 No Optimization With Optimization Model Mury time C++ time Mury time C++ time 2_peterson 0.05 13.26 0.05 13.25 abp 0.05 10.35 0.05 10.33 adash 0.17 114.18 3.28 113.84 adashbug 0.16 113.99 3.28 113.82 arbiter 0.04 11.35 0.05 11.38 cach3multi 0.02 0.02 0.02 0.02 cache3 0.09 54.27 0.51 54.14 dek 0.04 10.58 0.05 10.55 down 0.03 7.96 0.05 7.81 dp4 0.04 10.03 0.08 10.03 dpnew 0.05 12.15 0.06 12.10 eadash 0.15 97.00 1.55 96.89 ldash 0.09 77.32 1.26 77.25 lin 0.03 6.95 0.04 6.83 list6 0.04 21.63 0.10 21.40 list6too 0.05 30.93 0.27 30.81 mcslockl 0.05 20.38 0.08 20.40 mcslock2 0.06 28.61 0.09 28.67 n.peterson 0.05 16.46 0.06 16.42 newcache3 0.09 89.02 0.51 88.80 newlist6 0.05 38.61 0.07 38.45 ns 0.05 87.59 0.18 88.26 ns-old 0.06 87.36 0.19 87.47 pingpong 0.12 8.70 0.04 9.01 sci 0.77 245.46 7.98 246.74 scierr 0.77 244.36 7.69 243.30 sets 0.03 9.54 0.05 9.59 sort5 0.05 8.10 0.05 7.96 Table 5.8: Compilation times for example programs distributed with the Mury verifier, with hash compaction. 32 No Optimization With Optimization Model Muvip time C++ time Mury time C++ time student 1 0.06 57.53 0.34 57.24 student2 0.08 72.63 0.30 72.03 student3 0.07 69.44 0.29 69.49 student4 0.08 76.04 0.28 75.98 student5 0.06 47.54 0.20 47.70 student6 0.08 77.08 0.31 76.50 student7 0.11 91.22 2.48 84.84 student8 0.09 72.77 1.50 69.65 student9 0.09 72.72 0.39 72.80 studentlO 0.07 71.56 0.64 70.88 student11 0.07 49.33 0.22 49.38 Table 5.9: Compilation times for cache coherence protocol models, without hash compaction. No Optimization With Optimization Model Mury time C++ time Mur<£ time C++ time student 1 0.06 58.57 0.28 58.64 student2 0.08 73.82 0.30 73.18 student3 0.09 70.58 0.30 70.61 student4 0.08 77.19 0.29 77.29 student5 0.06 48.92 0.21 48.71 student6 0.08 78.36 0.31 77.56 student7 0.11 92.61 2.48 86.42 student8 0.08 74.02 1.51 70.90 student9 0.09 74.07 0.40 73.96 studentlO 0.08 72.75 0.64 71.98 student 11 0.07 50.77 0.22 50.55 Table 5.10: Compilation times for cache coherence protocol models, with hash com-paction. 33 Model No Optii Mur¥> time T i i z a t i o n C++ time With Opt Muif time imization C++ time 1394 0.07 37.08 0.46 35.38 Table 5.11: Compilation times for a model of part of the IEEE 1394 protocol, without hash compaction. Model No Optii Mur</? time nization C++ time With Opt Mur</> time imization C++ time 1394 0.08 38.22 0.43 36.41 Table 5.12: Compilation times for a model of part of the IEEE 1394 protocol, with hash compaction. 34 C h a p t e r 6 Conclusions and Future Work In this thesis, we assert that closing the gap between novice and expert is an impor-tant area for verification research. Novices model problems differently than experts, primarily because they understand less about the underlying tool. We have identi-fied several source-level transformations which promise to improve the verification experience for novice users. After creating the necessary infrastructure to work with Mury 3.1, we implemented one of those transformations to provide a preliminary test of our hypothesis. As we have seen, even a single source-level transformation was able to signifi-cantly improve several models written by novices. This result supports the assertions that novice users are likely to model systems differently and less efficiently for formal verification, that many of these inefficient modeling choices can be easily detected at the source-code level, and that a verification tool can optimize away these inef-ficient modeling choices, thereby boosting the productivity of novice users. A tool user should not need to understand the inner details of the tool, nor adapt to those details, in order to use it effectively. This work is a step towards closing the gap 35 between novice and expert. Our goal was to illustrate how verification tools should adapt to novice users, rather than to advocate a specific optimization for a specific tool. Nevertheless, the most obvious direction for future work is to try the other proposed transformations and measure their effectiveness. Doing so with Mur</? 3.1 would require a great deal of additional effort. We made a major planning mistake during this project: choosing to modify the existing Mur<£> 3.1 compiler rather than writing our own parser. The Mmf language is quite large. We chose to avoid the devil we knew, hoping that the underlying code would be easier to manipulate. Then, as the project progressed and the problems mounted, we chose to press on, believing that the next big obstacle would be the last. In retrospect, writing our own source-to-source compiler would have been easier. Given the structural problems with Mur<£> 3.1, future source-level optimiza-tion work should follow one of two approaches. Creating a source-to-source optimizer is the simpler of the two, and has the advantage that Muvp 3.1 would still be used for code generation, ensuring compatibility. The more comprehensive approach is to rewrite Mury, maintaining rigid separation between parsing, optimization, and code generation. Although there are greater drawbacks to a full rewrite, including the effort of developing a full compiler and of ensuring compatibility with existing Mur<£> compilers, the final result would be a more powerful tool. The more general direction for future work, and the promise of greater im-pact, is to apply these ideas to other verification tools and languages. Possible questions to investigate include what source-level changes might reduce BDD size, what aspects of Verilog or VHDL might highlight easy-to-implement optimizations, 36 and how might a future hardware description language or verification language be best designed to support robust ease-of-use. Considerable further research needs to be done. 37 Bibliography [1] Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986. [2] Randal E. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. Technical Report CMU-CS-92-160, Carnegie Mellon University, July 1992. A version of this report was published in Computing Surveys, Vol. 24, No. 3, September 1992, p. 293-318. [3] K. Mani Chandy and Jayadev Misra. Parallel Program Design - a foundation. Addison-Wesley, 1988. [4] E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. [5] David L. Dill. The Mury? verification system. In R. Alur and T. A. Hen-zinger, editors, Computer-Aided Verification: Eighth International Conference, pages 390-393. Springer-Verlag, July 1996. Lecture Notes in Computer Science Number 1102. [6] David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang. Protocol verification as a hardware design aid. In International Conference on Computer Design. IEEE, October 1992. [7] David L. Dill, Seungjoon Park, and Andreas G. Nowatzyk. Formal specification of abstract memory models. In Research on Integrated Systems: Proceedings of the 1993 Symposium, pages 38-52. MIT Press, 1993. Seattle, Washington, March 14-16. [8] Aarti Gupta. Formal hardware verification methods: A survey. Formal Methods in System Design, 1:151-238, 1992. [9] Alan J. Hu. Formal hardware verification with BDDs: An introduction. In Pacific Rim Conference on Communications, Computers, and Signal Processing (PACRIM), pages 677-682. IEEE, 1997. 38 [10] Alan J. Hu, Masahiro Fujita, and Chris Wilson. Formal verification of the HAL SI system cache coherence protocol. In International Conference on Computer Design, pages 438-444. IEEE, 1997. [11] Alan J. Hu, Rui Li, Xizheng Shi, and Son Vuong. Model checking a se-cure group communication protocol: A case study. In Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV). IFIP TC6/WG6.1, 1999. [12] Cable PHY specification, pages 49-112. In IEEE Std 1394-1995 [13], August 1996. [13] IEEE Standard for a High Performance Serial Bus. IEEE Std 1394-1995. Insi-titute of Electrical and Electronics Engineers, 345 East 47th Street, New York, NY 10017, USA, August 1996. [14] C. Norris Ip. Using symbolic analysis to optimize explicit reachability analysis. In IEEE International High Level Design Validation and Test Workshop, pages 130-137. IEEE, 1999. [15] C. Norris Ip and David L. Dill. Efficient verification of symmetric concurrent systems. In International Conference on Computer Design, pages 230-234. IEEE, October 1993. [16] Jawahar Jain, Amit Narayan, Masahiro Fujita, and Alberto Sangiovanni-Vincentelli. Formal verification of combinational circuits. In International Conference on VLSI Design, 1997. [17] Christoph Kern and Mark R. Greenstreet. Formal verification in hardware design: A survey. ACM Transactions on Design Automation of Electronic Systems, 4(2):123-193, April 1999. [18] John C. Mitchell, Mark Mitchell, and Ulrich Stern. Automated analysis of cryptographic protocols using Mury. In Symposium on Security and Privacy, pages 141-151. IEEE, 1997. [19] John C. Mitchell, Vitaly Shmatikov, and Ulrich Stern. Finite-state analysis of SSL 3.0. In 7th USENIX Security Symposium, January 1998. [20] Steven S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997. 39 [21] Steven S. Muchnick. Interprocedural Data-Flow Analysis, pages 619-637. In Advanced Compiler Design and Implementation [20], 1997. [22] Steven S. Muchnick. Live Variables Analysis, pages 443-446. In Advanced Compiler Design and Implementation [20], 1997. [23] Steven S. Muchnick. Loop distribution, page 694. In Advanced Compiler Design and Implementation [20], 1997. [24] Steven S. Muchnick. Removal of Induction Variables and Linear-Function Test Replacement, pages 447-453. In Advanced Compiler Design and Implementation [20], 1997. [25] Lawrence Yang, David Gao, Jamshid Mostoufi, Raju Joshi, and Paul Loewen-stein. System design methodology of UltraSPARC-I. In 32nd Design Automa-tion Conference, pages 7-12. ACM/IEEE, 1995. [26] Karen Yorav and Orna Grumberg. Static analysis for state-space reductions preserving temporal logics. Technical Report CS-2000-03, The Technion, Haifa, Israel, 2000. 40 A p p e n d i x A M u r ^ Optimizer Source This appendix contains full source code for our Mury optimizer. The source is available electronically,1 but it is included here for archival purposes. The Internet is a powerful dynamic communication medium, but is not well suited for long term data preservation. The last ten years have seen the demise of several file location protocols (e.g., gopher and archie); it is unlikely that HTTP will fare better over time. The ruleset rearrangement transformation is implemented as a modification of Mury 3.1. The modifications to the Mury 3.1 compiler itself are minimal, and listed in Section A.3.1 in unified diff format. The bulk of the optimizer mirrors the structure of the Mury parse tree, with methods for manipulating the tree and for updating the necessary Mury 3.1 data structures for code generation. C++ header files are presented first, followed by the associated C++ code files and finally other support files. 1At publication time, from http://www.cs.ubc.ca/labs/isd/Projects/. 41 A . l C++ Header Files A . l . l mu_opt.h / / mu_opt.h -*- C++ - * -#i fndef MU.OPT.H #define MU.OPT.H / / # i n c l u d e "mu.opt .base .h" / / # i n c l u d e " m u . o p t . s t e . h " / / S i n c l u d e "rau_opt_stmt.h" / / # i n c l u d e " m u . o p t . d e c l . h " / / # i n c l u d e "mu_opt_rule .h" # inc lude "mu_opt_root .h" ftendif / * MU.OPT.H * / # i fndef MU.OPT.BASE.H #define MU.OPT.BASE.H # inc lude <mu.h> # inc lude <iostream.h> # inc lude < l i s t > # inc lude <set> / / # d e f i n e MUOPT.DEBUG typedef uns igned i n t u i n t ; typedef set<int> ScopeSet; c l a s s MuOptObject; typedef s t r u c t { v o i d *node; / / new c h i l d Murphi ob jec t MuOptObject * o b j ; / / new c h i l d muopt o b j e c t } OptRet; c l a s s MuOptObject { p u b l i c : MuOptObject(const char *name = NULL); v i r t u a l "MuOptObj e c t ( ) ; const char *name() const -[ r e t u r n .name; } v i r t u a l v o i d d i sp layTree(os tream& out , u i n t indent ) const = 0 ; v i r t u a l ScopeSet *deps(u int reqNum = 0 ) const = 0 ; v i r t u a l OptRet o p t i m i z e O ; i n t depLoop(uint reqNum) const ; s t a t i c u i n t nextReqNumQ { r e t u r n ++_thisReqNum; } A . 1.2 mu_opt_base.h / / mu_opt .base .h C++ - * -42 s t a t i c v o i d indentLine(ostream& out , u i n t i n d e n t ) ; p r i v a t e : char *_name; mutable u i n t _lastReqNum; s t a t i c u i n t _thisReqNum; }; #endif / * MU.OPT.BASE.H * / A.1.3 mu_opt_decl.h / / rau_opt_decl .h - * - C + + - * -#i fndef MU_OPT_DECL_H #define MU_OPT_DECL_H # inc lude "mu_opt_base.h" # inc lude "mu_opt_ste.h" # inc lude "mu_opt_stmt.h" (( include <map> c l a s s MuOptTypeDecl; c l a s s MuOptDecl : p u b l i c MuOptObject { p u b l i c : enum Type { T y p e D e c l , Cons t , V a r , A l i a s , Quant, Choose, Param, P r o c , Func , E r r o r , unknown }; p r o t e c t e d : MuOptDecl(Type t , const char *name) : MuOptObject(name), _ type ( t ) { } p u b l i c : v i r t u a l "MuOptDecl( ) ; Type t y p e Q const { r e t u r n _type; } s t a t i c MuOptDecl * n e « M u O p t D e c l ( d e c l * ) ; p r i v a t e : Type _ type; s t a t i c map<decl*,MuOptDecl*> . e x i s t i n g ; }; c l a s s MuOptDeclConst : p u b l i c MuOptDecl { p u b l i c : MuOptDec lCons t (cons tdec l *n) ; v i r t u a l "MuOptDeclConst( ) ; v i r t u a l v o i d displayTree(ostreara& out , u i n t indent ) const ; v i r t u a l ScopeSet *deps(u int reqNum = 0) cons t ; p r i v a t e : c o n s t d e c l *_node; / / do not own MuOptTypeDecl *_typed; }; c l a s s MuOptDeclVar : p u b l i c MuOptDecl { 43 public: MuOptDeclVar(vardecl *n); v ir tua l "MuOptDeclVar(); v ir tua l void displayTree(ostream& out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: vardecl *_node; / / d o not own MuOptTypeDecl *_typed; } ; class MuOptDeclAlias : public MuOptDecl { public: MuOptDeclAliasCaliasdecl *n); v ir tua l "MuOptDeclAlias(); v i r tua l void displayTree(ostream& out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private; al iasdecl *_node; / / do not own MuOptExpr _ref; } ; class MuOptDeclQuant : public MuOptDecl { public: MuOptDeclQuant(quantdecl *n); v i r tua l "MuOptDeclQuant(); v i r tua l void displayTree(ostream& out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: quantdecl *_node; / / d o not own MuOptTypeDecl *_typed; MuOptExpr . l e f t ; MuOptExpr . r ight ; } ; class MuOptDeclChoose : public MuOptDecl { public: MuOptDeclChoose(choosedecl *n); v i r tua l "MuOptDeclChoose(); v ir tua l void displayTree(ostream& out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: choosedecl *_node; / / d o not own MuOptTypeDecl *_typed; } ; class MuOptDeclProc ; public MuOptDecl { public: MuOptDeclProc(procdecl *n); v i r tua l "MuOptDeclProc(); v i r tua l void displayTree(ostreamft out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; 44 p r i v a t e : p r o c d e c l *_node; / / d o not own MuOptSTEChain _params; MuOptSTEChain _ d e c l s ; MuOptStmtList . b o d y ; } ; c l a s s MuOptDeclFunc : p u b l i c MuOptDecl { p u b l i c : MuOptDeclFunc( funcdec l *n) ; v i r t u a l "MuOptDeclFunc(); v i r t u a l v o i d displayTree(ostreamfc out , u i n t indent) const v i r t u a l ScopeSet *deps (u int reqNum = 0 ) const ; p r i v a t e : f u n c d e c l *_node; / / do not own MuOptSTEChain .params; MuOptSTEChain . d e c l s ; MuOptStmtList .body; MuOptDecl * _ r e t u r n t y p e ; }; c l a s s MuOptDeclError : p u b l i c MuOptDecl { p u b l i c : M u O p t D e c l E r r o r ( e r r o r . d e c l * n ) ; v i r t u a l " M u O p t D e c l E r r o r O ; v i r t u a l v o i d d i sp layTree (os t ream& out , u i n t indent ) const v i r t u a l ScopeSet *deps (u in t reqNum = 0 ) cons t ; p r i v a t e : e r r o r . d e c l *_node; / / do not own } ; #endif / * MU.OPT.DECL.H * / A . 1.4 mu_opt_expr.h / / mu .opt . expr . h - * - C + + - * -#ifndef MU.OPT.EXPR.H t d e f i n e MU.OPT.EXPR.H ftinclude " m u . o p t . b a s e . h" #include " m u . o p t . s t e . h " c l a s s MuOptExpr : p u b l i c MuOptObject { p u b l i c : MuOptExpr(expr *e) ; v i r t u a l " M u O p t E x p r O ; v i r t u a l v o i d d i s p l a y T r e e ( o s t r e a m _ out , u i n t indent) const v i r t u a l ScopeSet *deps (u in t reqNum = 0 ) cons t ; p r i v a t e : expr *_node; / / d o not own 45 MuOptSTEChain *_used; } ; c l a s s MuOptDesignator -( p u b l i c : MuOptDesignator() { } v i r t u a l "MuOptDesignator() ; v i r t u a l v o i d d isplayTree(ostreamft ou t , u i n t indent ) const = 0; v i r t u a l ScopeSet *deps (u int reqNum = 0) const = 0; v i r t u a l b o o l i s L i s t O const = 0; s t a t i c MuOptDesignator *newMuOptDesignator(designator * ) ; } ; c l a s s MuOptDesignatorInstance : p u b l i c MuOptExpr, p u b l i c MuOptDesignator { p u b l i c : MuOptDes ignatorIns tance (des ignator *d ) ; v i r t u a l "MuOptDes ignator lns tanceQ ; v i r t u a l v o i d d i sp layTree (os tream& out , u i n t indent ) cons t ; v i r t u a l ScopeSet *deps (u int reqNum = 0) cons t ; b o o l i s L i s t O const ; p r i v a t e : MuOptSTE . o r i g i n ; MuOptExpr . a r r a y r e f ; MuOptSTE _ f i e l d r e f ; } ; c l a s s MuOptExprLis t : p u b l i c MuOptObject { p u b l i c : M u O p t E x p r L i s t ( e x p r l i s t *e); v i r t u a l " M u O p t E x p r L i s t ( ) ; v i r t u a l v o i d d i sp layTree (os tream& out , u i n t indent ) cons t ; v i r t u a l ScopeSet *deps (u int reqNum = 0) cons t ; p r i v a t e : l ist<MuOptExpr*> . l i s t ; } ; c l a s s MuOptDes ignatorLi s t : p u b l i c MuOptObject , p u b l i c MuOptDesignator { p u b l i c : M u O p t D e s i g n a t o r L i s t ( d e s i g n a t o r *d ) ; v i r t u a l " M u O p t D e s i g n a t o r L i s t O ; v i r t u a l v o i d displayTree(ostreamfe out , u i n t indent ) cons t ; v i r t u a l ScopeSet *deps (u int reqNum = 0) cons t ; b o o l i s L i s t O cons t ; p r i v a t e : l i s t<MuOptDes ignatorInstance*> . l i s t ; } ; #endif / * MU.OPT.EXPR.H * / 46 A.1.5 mu_opt_param.h / / mu_opt_param.h - * - c++ - * -# i fndef MU_OPT_PARAM_H t d e f i n e MU_OPT_PARAM_H t i n c l u d e "mu_opt_decl .h" # inc lude <map> c l a s s MuOptParam : p u b l i c MuOptDecl •( p u b l i c : enum Type { V a l u e , V a r , Cons t , /*Name,*/ E r r o r , unknown }; p r o t e c t e d : fj MuOptParam(Type t , const char *name); p u b l i c : v i r t u a l "MuOptParamO ; Type t y p e O const { r e t u r n _type; } v i r t u a l v o i d d isplayTree(ostreamft out , u i n t indent ) cons t ; s t a t i c MuOptParam *newMuOptParam(param * ) ; p r i v a t e : Type _type; s t a t i c map<param*,MuOptParam*> . e x i s t i n g ; }; c l a s s MuOptParamValue : p u b l i c MuOptParam { p u b l i c : MuOptParamValue(valparam * ) ; v i r t u a l "MuOptParamValue(); v i r t u a l v o i d d i sp layTree (os tream& out , u i n t i n d e n t ) cons t ; v i r t u a l ScopeSet *deps (u int reqNum = 0) c o n s t ; p r i v a t e : valparam *_node; / / d o not own }; c l a s s MuOptParamVar : p u b l i c MuOptParam •[ p u b l i c : MuOptParamVar(varparam * ) ; v i r t u a l "MuOptParamVar(); v i r t u a l v o i d d i sp layTree(os tream& out , u i n t indent ) cons t ; v i r t u a l ScopeSet *deps (u int reqNum = 0) c o n s t ; p r i v a t e : varparam *_node; / / do not own } ; c l a s s MuOptParamConst : p u b l i c MuOptParam { p u b l i c : MuOptParamConst(constparam * ) ; v i r t u a l "MuOptParamConst(); v i r t u a l v o i d d i sp layTree (os tream& out , u i n t indent ) cons t ; 47 v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: constparam *_node; / / do not own }; / * class MuOptParamName : public MuOptParam -( public: MuOptParamName(nameparam *); v i r tua l "MuOptParamName(); v i r tua l void displayTree(ostream& out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: nameparam *_node; / / do not own }; */ class MuOptParamError : public MuOptParam { public: MuOptParamError(param *); v i r t u a l "MuOptParamError(); v i r t u a l void displayTree(ostream& out, uint indent) const v i r t u a l ScopeSet *deps(uint reqNum = 0) const; private: param *_node; / / d o not own } ; #endif / * MU_0PT_PARAM_H * / A . 1.6 mu_opt_root.h / / mu_opt_root .h - * - C++ - * -#ifndef MU_0PT_R00T_H #define MU.0PT.R00T.H tinclude "mu_opt_base.h" #include "mu_opt_ste.h" #include "mu_opt_rule.h" class MuOptRoot { public: MuOptRoot(program *prog); v i r t u a l "MuOptRoot(); void displayTree(ostream& out = cout) const; ScopeSet *deps() const; void optimizeO; private: program *_prog; / / do not own MuOptSTEChain *_globals; 48 MuOptSTEChain *_procedures; MuOptRuleList *_rules; } ; #endif / * MU_OPT_ROOT_H * / A.1.7 mu_opt_rule.h / / mu_opt_rule.h - * - C++ - * -ftifndef MU_OPT_RULE_H #define MU.OPT.RULE.H #include "mu_opt_base.h" tinclude "mu_opt_ste.h" #include "mu_opt_expr.h" #include "mu_opt_stmt .h" / / bogus class so I can have a single pointer for rules and rule l i s t s / / without going a l l the way up to MuOptObject class MuOptRuleBase : public MuOptObject { public: MuOptRuleBase(const char *name = NULL) : MuOptObject(name) { } v i r t u a l "MuOptRuleBase(); v i r tua l bool i s L i s t O const = 0; v ir tua l void rebuildRulelnfo(const ScopeSet *encl) = 0; } ; class MuOptRule : public MuOptRuleBase { public: enum Type { Simple, Startstate, Invar, Quant, Choose, Al ias , F a i r , Live }; protected: MuOptRule(Type type, const char *name, rule *node) : MuOptRuleBase(name), _type(type), _node(node) •£ } public: v i r tua l "MuOptRule(); Type type() const { return _type; } rule *node() { return _node; } bool i s L i s t O const; stat ic MuOptRule *newMuOptRule(rule*); s tat ic MuOptRule *newMuOptRule(MuOptRule*); private: Type _type; rule *_node; } ; class MuOptRuleList: public MuOptRuleBase { public: MuOptRuleList(rule*); MuOptRuleList(const MuOptRuleList* = NULL); v i r tua l "MuOptRuleList(); 49 v ir tua l void displayTree(ostream& out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; v i r tua l OptRet optimizeO; v ir tua l void rebuildRulelnfo(const ScopeSet *encl); void split(MuOptRule*& car, MuOptRuleList*. cdr) const; MuOptRule *pop_front(); void append(MuOptRule* r ) ; void append(const MuOptRuleList* r l ) ; uint s i zeQ const -( return . l i s t . size () ; } bool i s L i s t O const; private: list<MuOptRule*> _ l i s t ; } ; class MuOptRuleSimple : public MuOptRule { public: MuOptRuleSimple(simplerule*); protected: MuOptRuleSimple(simplerule*, Type); public: v i r tua l "MuOptRuleSimpleO ; v i r tua l void displayTree(ostream& out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; v i r tua l void rebuildRulelnfo(const ScopeSet *encl); v i r tua l const char *typeName() const; private: MuOptSTEChain .enclosures; MuOptExpr .condition; MuOptSTEChain . loca l s ; MuOptStmtList .body; bool .unfair; } ; class MuOptRuleStartstate : public MuOptRuleSimple { public: MuOptRuleStartstate(startstate*); v ir tua l "MuOptRuleStartstateO; v i r tua l const char *typeName() const; } ; class MuOptRuleInvar : public MuOptRuleSimple { public: MuOptRuleInvar(invariant*); v ir tua l "MuOptRulelnvarO ; v ir tua l const char *typeName() const; } ; class MuOptRuleQuant : public MuOptRule { public: MuOptRuleQuant(quantrule*); v ir tua l "MuOptRuleQuant(); 50 vir tua l void displayTree(ostream& out, uint indent) const v ir tual ScopeSet *deps(uint reqNum = 0) const; v ir tua l OptRet optimizeO; v ir tua l void rebuildRulelnfo(const ScopeSet *encl); int scope() const { return _quant. scopeO ; } private: MuOptSTE _quant; MuOptRuleBase *_rules; } ; class MuOptRuleChoose : public MuOptRule { public: MuOptRuleChoose(chooserule*); v ir tua l "MuOptRuleChoose(); v i r tua l void displayTree(ostream& out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; v i r tua l OptRet optimizeO; v i r tua l void rebuildRulelnfo(const ScopeSet *encl); int scopeO const { return _index. scopeO; } private: MuOptSTE .index; MuOptDesignator *_set; MuOptRuleBase *_rules; }; class MuOptRuleAlias : public MuOptRule { public: MuOptRuleAlias(aliasrule*); v ir tua l "MuOptRuleAlias(); v ir tua l void displayTree(ostream& out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; v ir tua l OptRet optimizeO; v ir tua l void rebuildRulelnfo(const ScopeSet *encl); int scopeO const { return .al iases.scopeO ; } private: MuOptSTE .a l iases; MuOptRuleBase *_rules; } ; class MuOptRuleFair : public MuOptRule { public: MuOptRuleFair(fairness*); v ir tua l "MuOptRuleFair(); v ir tua l void displayTree(ostreamft out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; v ir tual void rebuildRulelnfo(const ScopeSet *encl); } ; class MuOptRuleLive : public MuOptRule { public: 51 MuOptRuleLive(liveness*); v ir tua l "MuOptRuleLive(); v ir tua l void displayTree(ostreamfc out, uint indent) const; v ir tua l ScopeSet *deps(uint reqNum = 0) const; v ir tual void rebuildRulelnfo(const ScopeSet *encl); } ; #endif / * MU_0PT_RULE_H * / A.1 .8 mu_opt_ste.h / / mu_opt_ste.h - * - C + + - * -#ifndef MU_0PT_STE.H #define MU_0PT_STE_H tinclude "mu_opt_base.h" class MuOptDecl; class MuOptSTE : public MuOptObject { public: MuOptSTE(ste *s); v ir tual "MuOptSTEO; v ir tual void displayTree(ostream& out, uint indent) const; v ir tual ScopeSet *deps(uint reqNum = 0) const; int scopeO const { return .scope; } ste *node() { return _node; } private: ste *_node; / / do not own int _scope; int .lextype; MuOptDecl *_value; } ; class MuOptRuleSimple; / / HACK: need to do some funky stuff to Murphi side / / for some of the rule optimizations *+*+* class MuOptSTEChain : public MuOptObject { public: / / run from start up to but not including stop MuOptSTEChain(ste *start, ste *stop=NULL); MuOptSTEChain(stelist *start, s te l i s t *stop=NULL); MuOptSTEChain(stecoll *s); v ir tua l "MuOptSTEChain(); v ir tua l void displayTree(ostream& out, uint indent) const; v ir tua l ScopeSet *deps(uint reqNum = 0) const; ScopeSet *scopes() const; private: 52 list<MuOptSTE*>fc chainQ { return .chain; > friend MuOptRuleSimple; private: list<MuDptSTE*> .chain; } ; #endif / * MU.OPT.STE.H * / A.1.9 mu_opt_stmt.h / / mu.opt.stmt .h - * - C + + - * -#ifndef MU.OPT.STMT.H #define MU.OPT.STMT.H #include "mu_opt.base.h" #include "mu.opt.expr.h" #include <map> class MuOptStmt : public MuOptObject { public: enum Type { Assignment, While, If, Case, Switch, For, Proc, Clear, Error Assert, Put, Al ias , Aliasstmt, Return, Undefine, MultisetAdd MultisetRemove, Nul l , unknown }; protected: MuOptStmt(Type t) : _type(t) { } public: v i r tua l "MuOptStmt(); Type typeO const { return .type; } static MuOptStmt *newMuOptStmt(stmt *); private: Type .type; static map<stmt*,MuOptStmt*> .exist ing; } ; class MuOptStmtList : public MuOptObject { public: MuOptStmtList(stmt *s) ; v ir tua l "MuOptStmtList(); v ir tua l void displayTree(ostreamft out, uint indent) const; v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: list<MuOptStmt*> . l i s t ; } ; class MuOptStmtAssignment : public MuOptStmt { public: MuOptStmtAssignment(assignment *a); v i r tua l "MuOptStmtAssignmentO ; v ir tua l void displayTree(ostream& out, uint indent) const; 53 v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: assignment *_node; / / d o not own MuOptExpr _src; MuOptDesignator *_target; } ; class MuOptStmtWhile : public MuOptStmt { public: MuOptStmtWhile(whilestmt *w); v i r tua l "MuOptStmtWhile(); v i r tua l void displayTree(ostream& out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: whilestmt *_node; / / d o not own MuOptExpr _test; MuOptStmtList _body; }; class MuOptStmtlf : public MuOptStmt { public: MuOptStmtlf(ifstmt * i ) ; v i r t u a l "MuOptStmtlf(); v i r t u a l void displayTree(ostream& out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: ifstmt *_node; / / do not own MuOptExpr _test; MuOptStmtList .body; MuOptStmtList .else; } ; class MuOptStmtCase : public MuOptStmt { public: MuOptStmtCase(caselist *c); v i r t u a l "MuOptStmtCase(); v i r t u a l void displayTree(ostream& out, uint indent) const v i r t u a l ScopeSet *deps(uint reqNum = 0) const; private: caselist *_node; / / d o not own MuOptExprList .values; MuOptStmtList .body; } ; class MuOptStmtCaseList : public MuOptObject { public: MuOptStmtCaseList(caselist *c); v i r t u a l "MuOptStmtCaseList(); v i r t u a l void displayTree(ostream& out, uint indent) const v i r t u a l ScopeSet *deps(uint reqNum = 0) const; private: 54 list<MuOptStmtCase*> . l i s t ; };' class MuOptStmtSwitch : public MuOptStmt { public: MuOptStmtSwitchCswitchstmt *s); v ir tua l •MuOptStmtSwitchO ; v i r tua l void displayTree(ostreamfc out, uint indent) const; v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: switchstmt *_node; / / do not own MuOptExpr _expr; MuOptStmtCaseList .cases; MuOptStmtList .default; } ; class MuOptStmtFor : public MuOptStmt { public: MuOptStmtFor(forstmt *f); v i r tua l "MuOptStmtFor(); v i r tua l void displayTree(ostreamfe out, uint indent) const; v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: forstmt *_node; / / do not own MuOptSTEChain .index; MuOptStmtList .body; } ; class MuOptStmtProc : public MuOptStmt { public: MuOptStmtProc(proccall *p); v i r t u a l "MuOptStmtProc(); v i r t u a l void displayTree(ostreamft out, uint indent) const; v i r t u a l ScopeSet *deps(uint reqNum = 0) const; private: proccal l *_node; / / do not own MuOptSTE .procedure; MuOptExprList .actuals; } ; class MuOptStmtClear : public MuOptStmt { public: MuOptStmtClear(clearstmt *c); v i r t u a l "MuOptStmtClear(); v i r tua l void displayTree(ostreamft out, uint indent) const; v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: clearstmt *_node; / / do not own MuOptDesignator *_target; } ; class MuOptStmtError : public MuOptStmt •{ 55 public: MuOptStmtError(errorstmt *e); protected: MuOptStmtError(errorstmt *e, bool isAssert); public: v ir tua l "MuOptStmtError(); v i r tua l void displayTree(ostream_ out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; protected: const char *errstring() const { return . s tr ing; } private: errorstmt *_node; / / d o not own const char *_string; / / do not own } ; class MuOptStmtAssert : public MuOptStmtError { public: MuOptStmtAssert(assertstmt *a); v ir tua l "MuOptStmtAssert(); v ir tua l void displayTree(ostreamft out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: assertstmt *_node; / / do not own MuOptExpr _test; } ; class MuOptStmtPut : public MuOptStmt {. public: MuOptStmtPut(putstmt *p); v i r tua l "MuOptStmtPut(); v i r tua l void display Tree (ostreamSt out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: putstmt *_node; / / do not own } ; class MuOptStmtAlias : public MuOptStmt { public: MuOptStmtAlias(alias *a); v ir tua l "MuOptStmtAliasO; v ir tua l void displayTree(ostream_ out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: al ias *_node; / / d o not own } ; class MuOptStmtAliasstmt : public MuOptStmt -{ public: MuOptStmtAliasstmt(aliasstmt *a) ; v ir tua l "MuOptStmtAliasstmtO ; 56 virtual void displayTree(ostream& out, uint indent) const; v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: aliasstmt *_node; / / do not own MuOptSTEChain .al iases; MuOptStmtList _body; } ; class MuOptStmtReturn : public MuOptStmt { public: MuOptStmtReturn(returnstmt *r) ; v ir tua l "MuOptStmtReturnO ; v ir tua l void displayTree(ostreamSk out, uint indent) const; v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: returnstmt *_node; / / d o not own MuOptExpr _retexpr; } ; class MuOptStmtUndef ine : public MuOptStmt •[ public: MuOptStmtUndefine(undefinestmt *u) ; v ir tua l "MuOptStmtUndefine(); v ir tua l void displayTree(ostream& out, uint indent) const; v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: undefinestmt *_node; / / do not own MuOptDesignator *_target; } ; class MuOptStmtMultisetAdd : public MuOptStmt { public: MuOptStmtMultisetAdd(multisetaddstmt *m); v i r tua l "MuOptStmtMultisetAddO ; v ir tua l void displayTree(ostreamfe out, uint indent) const; v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: multisetaddstmt *_node; / / do not own MuOptDesignator *_element; MuOptDesignator *_target; } ; class MuOptStmtMultisetRemove : public MuOptStmt { public: MuOptStmtMultisetRemove(multisetremovestmt *m); v i r tua l "MuOptStmtMultisetRemove(); v ir tua l void displayTree (ostreamSk out, uint indent) const; v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: multisetremovestmt *_node; / / do not own MuOptSTE _index; 57 MuOptDesignator *_target; MuOptExpr _cri ter ion; } ; class MuOptStmtNull : public MuOptStmt { public: MuOptStmtNull(); v i r tua l "MuOptStmtNull(); v ir tua l void displayTree(ostream& out, uint indent) const; v ir tua l ScopeSet *deps(uint reqNum = 0) const; } ; #endif / * MU.OPT.STMT.H * / A.1.10 mu_opt_typedecl.h / / mu.opt.typedecl.h - * - C++ - * -#ifndef MU.OPT.TYPEDECL.H #define MU.OPT.TYPEDECL.H #include "mu.opt.decl.h" #include <map> class MuOptTypeDecl : public MuOptDecl { public: enum Type { Enum, Range, Array, Multiset, MultiSetID, Record, Scalarset, Union, Error, unknown }; protected: MuOptTypeDecl(Type t , const char *name) : MuOptDecKTypeDecl, name), _type(t) { } public: v ir tua l "MuOptTypeDeclO ; Type type() const { return .type; } static MuOptTypeDecl *newMuOptTypeDecl(typedecl *); v ir tua l void displayTree(ostream& out, uint indent) const;. private: Type .type; static map<typedecl*,MuOptTypeDecl*> .exist ing; } ; class MuOptTypeDeclEnum : public MuOptTypeDecl { public: MuOptTypeDeclEnum(enumtypedecl *n); v ir tua l "MuOptTypeDeclEnumO ; v ir tua l void displayTree(ostream& out, uint indent) const; v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: enumtypedecl *_node; / / do not own 58 int _left; int _right; MuOptSTEChain _idvalues; } ; class MuOptTypeDeclRange : public MuOptTypeDecl { public: MuOptTypeDeclRange(subrangetypedecl *n); v ir tua l "MuOptTypeDeclRange(); v i r tua l void displayTree(ostreamfe out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: subrangetypedecl *_node; / / d o not own int _left; int _right; } ; class MuOptTypeDeclArray : public MuOptTypeDecl { public: MuOptTypeDeclArray(arraytypedecl *n); v ir tua l "MuOptTypeDeclArray(); v ir tua l void displayTree(ostreamft out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: arraytypedecl *_node; / / do not own MuOptTypeDecl *_indexType; MuOptTypeDecl *_elementType; } ; class MuOptTypeDeclMultiSet : public MuOptTypeDecl { public: MuOptTypeDeclMultiSet(multisettypedecl *n) ; v ir tua l "MuOptTypeDeclMultiSet(); v ir tua l void displayTree(ostreamft out, uint indent) const v ir tua l ScopeSet *deps(uint reqNum = 0) const; private: multisettypedecl *_node; / / do not own }; class MuOptTypeDeclMultiSetID : public MuOptTypeDecl { public: MuOptTypeDeclMultiSetID(multisetidtypedecl *n); v i r tua l "MuOptTypeDeclMultiSetlDO ; v i r tua l void displayTree(ostreamfe out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: multisetidtypedecl *_node; / / do not own } ; class MuOptTypeDeclRecord : public MuOptTypeDecl { public: MuOptTypeDeclRecord(recordtypedecl *n); 59 v ir tua l "MuOptTypeDeclRecordO ; v i r tua l void displayTree(ostream. out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: recordtypedecl *_node; / / do not own MuOptSTEChain . f i e lds ; }; class MuOptTypeDeclScalarset : public MuOptTypeDecl { public: MuOptTypeDeclScalarset(scalarsettypedecl *n); v i r t u a l "MuOptTypeDeclScalarset(); v ir tua l void displayTree(ostream& out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: scalarsettypedecl *_node; / / do not own int . l e f t ; int . r ight ; MuOptSTE .idvalues; / / *+*+* should this be a chain? } ; class MuOptTypeDeclUnion : public MuOptTypeDecl { public: MuOptTypeDeclUnion(uniontypedecl *n); v i r tua l "MuOptTypeDeclUnion(); v i r tua l void displayTree(ostreamfc out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: uniontypedecl *_node; / / do not own MuOptSTEChain .unionmembers; } ; class MuOptTypeDeclError : public MuOptTypeDecl { public: MuOptTypeDeclError(errortypedecl *n); v i r t u a l "MuOptTypeDeclError(); v i r t u a l void displayTree(ostream& out, uint indent) const v i r tua l ScopeSet *deps(uint reqNum = 0) const; private: errortypedecl *_node; / / do not own } ; #endif / * MU.OPT.TYPEDECL.H * / 60 A.2 C-\—h Program Files A.2.1 mu_opt_base.cc / / mu_opt_base . cc - * - C + + - * -tinclude "mu_opt_base.h" uint MuOptObject::_thisReqNum = 0; MuOptObject::MuOptObject(const char *name) { if(name) { .name = new char [strlen(name) + 1]; strcpy(_name, name); y else .name = NULL; _lastReqNum = 0; } MuOptObject::"MuOptObject() { delete [] _name; > int MuOptObject::depLoop(uint reqNum) const { if(reqNum == _lastReqNum) return 1; _lastReqNum = reqNum; return 0; } void MuOptObject::indentLine(ostream& out, uint indent) { for(uint i = 0; i < indent; i++) out « " "; } OptRet MuOptObject:: optimizeO { / /assert(O); / / eventually I want to make this purely v i r tua l OptRet result; result.node = NULL; result .obj = NULL; return result; } A.2.2 mu_opt_decl.cc / / mu_opt_decl.cc - * - C + + - * -#include "mu_opt_decl-h" #include "mu_opt_param.h" ((include "mu_opt_typedecl.h" map<decl*,MuOptDecl*> MuOptDecl::_existing; 61 MuOptDecl::"MuOptDecl() { } MuOptDecl *MuOptDecl::newMuOptDecl(decl *d) { MuOptDecl *result = NULL; i f (d) i f ( .exist ing. f ind(d) == .existing.end()) {. switch(d->getclass()) { case decl::Type: result=MuOptTypeDecl::newMuOptTypeDecl(dynamic_cast<typedecl*>(d>); break; case decl: Const: result = new MuOptDeclConst(dynamic_cast<constdecl*>(d)); break; case decl: Var: result = new MuOptDeclVar(dynamic_cast<vardecl*>(d)); break; case decl: Al ias : result = new MuOptDeclAlias(dynamic_cast<aliasdecl*>(d)); break; case decl: Quant: result = new MuOptDeclQuant(dynamic_cast<quantdecl*>(d)); break; case decl: Choose: result = new MuOptDeclChoose(dynamic_cast<choosedecl*>(d)); break; case decl: Param: result = MuOptParam::newMuOptParam(dynamic_cast<param*>(d)); break; case decl: Proc: result = new MuOptDeclProc(dynamic_cast<procdecl*>(d)); break; case decl: Func: result = new MuOptDeclFunc(dynamic_cast<funcdecl*>(d)); break; case decl: Error .dec l : result = new MuOptDeclError(dynamic_cast<error_decl*>(d)); break; default: assert(O); } .existing[d] = result; } else i result = _existing[d]; #ifdef MUOPT.DEBUG cerr << "reissuing existing decl\n"; #endif } return result; } MuOptDeclConst::MuOptDeclConst(constdecl *n) : MuOptDecKConst, n ? n->name : NULL), _node(n), .typed(NULL) { #ifdef MUOPT.DEBUG cerr « "MuOptDeclConst::MuOptDeclConst(constdecl*)\n"; tendif / / i f ( n && n->gettype()) E / / .typed = MuOptTypeDecl::newMuOptTypeDecl(n->gettype()); 62 } MuOptDeclConst::"MuOptDeclConst() { / /delete _typed; } void MuOptDeclConst::displayTree(ostream& out, uint indent) const (tifdef MUOPT.DEBUG cerr << "MuOptDeclConst::displayTree(int) const\n"; #endif indentLine(out, indent); out << "decl_class is Const V " << nameO << "\"\n"; if(_typed) { indentLine(out, indent + 1); out << " [typed]\n"; _typed->displayTree(out, indent + 2); > } ScopeSet *MuOptDeclConst: :deps (uint reqNum = 0) const {, ScopeSet *resu l t ; / / , *temp; if(reqNum == 0) reqNum = nextReqNumO ; i f (depLoop (reqNum)) return new ScopeSet; if(.typed) result = _typed->deps(reqNum); else result = new ScopeSet; //temp = .deps(reqNum); //result->insert(temp->begin() , temp->endO) ; / /delete temp; return result; } MuOptDeclVar: -.MuOptDeclVar (vardecl *n) : MuOptDecKVar, n ? n->name : NULL), _node(n), .typed(NULL) { #ifdef MUOPT.DEBUG cerr « "MuOptDeclVar::MuOptDeclVar(vardecl*)\n"; #endif / / i f ( n && n->gettype()) / / .typed = MuOptTypeDecl::newMuOptTypeDecl(n->gettype()); } MuOptDeclVar::"MuOptDeclVar() { / /delete _typed; } void MuOptDeclVar::displayTree(ostreamSk out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptDeclVar::displayTree(int) const\n"; #endif indentLine(out, indent); out << "decl.class is Var \"" « nameO << "\"\n"; 63 if( .typed) { indentLine(out, indent + 1); out << " [typed]\n"; _typed->displayTree(out, indent + 2); } } ScopeSet *MuOptDeclVar::deps(uint reqNum = 0) const { ScopeSet *resu l t ; / / , *temp; if(reqNum == 0) reqNum = nextReqNumQ ; if(depLoop(reqNum)) return new ScopeSet; if(.typed) result = _typed->deps(reqNum); else result = new ScopeSet; //temp = .deps(reqNum); //result->insert(temp->begin(), temp->end()); / /delete temp; return result; MuOptDeclAlias::MuOptDeclAlias(aliasdecl *n) : MuOptDecl(Alias, n ? n->name : NULL), _node(n), _ref(n ? n->getexpr() : NULL) { #ifdef MUOPT.DEBUG cerr « "MuOptDeclAlias::MuOptDeclAlias(aliasdecl*)\n"; #endif } MuOptDeclAlias: :"MuOptDeclAliasO { } void MuOptDeclAlias::displayTree(ostreamft out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptDeclAlias::displayTree(int) const\n"; #endif indentLine(out, indent); out « "decl.class is Alias V " « name() « "\"\n"; indentLine(out, indent + 1); out « "ref\n"; _ref.displayTree(out, indent + 2); } ScopeSet *MuOptDeclAlias::deps(uint reqNum = 0) const { ScopeSet *resu l t ; / / , *temp; if(reqNum == 0) reqNum = nextReqNumQ ; if(depLoop(reqNum)) return new ScopeSet; 64 result = _ref.deps(reqNum); //temp = .deps(reqNum); //result->insert(temp->begin(), temp->end()); / /delete temp; return result; } MuOptDeclQuant::MuOptDeclQuant(quantdecl *n) : MuOptDecl(Quant, n ? n->name : NULL), _node(n), _typed(NULL), _left(n ? n->left : NULL), _right(n ? n->right : NULL) { #ifdef MUOPT.DEBUG cerr << "MuOptDeclQuant::MuOptDeclQuant(quantdecl*)\n"; #endif / / i f ( n fcfc n->type) / / _typed = MuOptTypeDecl::newMuOptTypeDecl(n->type); } MuOptDeclQuant::"MuOptDeclQuant() { / /delete .typed; } void MuOptDeclQuant::displayTree(ostream& out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptDeclQuant::displayTree(int) const\n"; #endif indentLine(out, indent); out « "decl.class is Quant V " << nameO « "\"\n"; if(.typed) { indentLine(out, indent + 1); out << "[typed]\n"; _typed->displayTree(out, indent + 2); > } ScopeSet *MuOptDeclQuant::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = .left.deps(reqNum); temp = .right.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; if( .typed) { temp = _typed->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; } return result; } 65 MuOptDeclChoose::MuOptDeclChoose(choosedecl *n) : MuOptDecKChoose, n ? n->name : NULL), _node(n), _typed(NULL) { #ifdef MUOPT.DEBUG cerr << "MuOptDeclChoose::MuOptDeclChoose(choosedecl*)\n"; tendif / / i f ( n fc& n->type) / / .typed = MuOptTypeDecl::newMuOptTypeDecl(n->type); } MuOptDeclChoose::"MuOptDeclChoose() { / /delete .typed; > void MuOptDeclChoose::displayTree(ostream& out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptDeclChoose: :displayTree(int) const\n"; #endif indentLine(out, indent); out << "decl.class is Choose \"" << nameO << "\"\n"; if( .typed) _typed->displayTree(out, indent + 1); } ScopeSet *MuOptDeclChoose: :deps (uint reqNum = 0) const •( ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = new ScopeSet; if( .typed) { temp = _typed->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; } return result; } MuOptDeclProc::MuOptDeclProc(procdecl *n) : MuOptDecKProc, n ? n->name : NULL), _node(n), _params(n ? n->params : NULL), _decls(n ? n->decls : NULL), _body(n ? n->body : NULL) { #ifdef MUOPT.DEBUG cerr « "MuOptDeclProc::MuOptDeclProc(procdecl*)\n" ; #endif } MuOptDeclProc : : "MuOptDeclProc ( ) { } void MuOptDeclProc: :displayTree(ostream& out, uint indent) const •( #ifdef MUOPT.DEBUG 66 cerr << "MuOptDeclProc::displayTree(int) const\n"; Sendif indentLine(out, indent); out << "decl_class is Proc \"" << name() << "\"\n"; if(_node 8tfc 0 /*+*+* need to verify that this is a l l val id */) { indentLine(out, indent + 1); out << "params\n"; _params.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "decls\n"; .decls.displayTree(out, indent + 2); indentLine(out, indent + 1); out « "body\n"; _body.displayTree(out, indent + 2); } } ScopeSet *MuOptDeclProc: : deps (uint reqNum = 0) const -C ScopeSet *result, *temp; i f (reqNum == 0) reqNum - nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; / / This is sort of a shotgun approach. In theory nothing above th i / / point should ever have dependencies on things l ike the scope of / / params. result = _params.deps(reqNum); temp = _decls.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; temp = _body.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; MuOptDeclFunc::MuOptDeclFunc(funcdecl *n) : MuOptDecKProc, n ? n->name : NULL), _node(n), _params(n ? n->params : NULL), _decls(n ? n->decls : NULL), _body(n ? n->body : NULL), _returntype(NULL) { #ifdef MUOPT.DEBUG cerr << "MuOptDeclFunc::MuOptDeclFunc(funcdecl*)\n"; tendif if(.node) { .returntype = MuOptDecl::newMuOptDecl(_node->returntype); assert(.returntype); } } MuOptDeclFunc::"MuOptDeclFunc() { / /delete .returntype; } 67 void MuOptDeclFunc::displayTree(ostream& out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptDeclFunc::displayTree(int) const\n"; #endif indentLine(out, indent); out << "decl.class is Func \"" << nameO << "\"\n"; if(.node) { indentLine(out, indent + 1); out << "params\n"; .params.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "decls\n"; .decls .displayTree(out, indent + 2); indentLine(out, indent + 1); out « "body\n"; .body.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "returntype\n" ; _returntype->displayTree(out, indent + 2); } ScopeSet *MuOptDeclFunc::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum ==0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = .params.deps(reqNum); temp = .decls.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; temp = .body.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; temp = _returntype->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; MuOptDeclError:;MuOptDeclError(error_decl *n) : MuOptDecl(Error, n ? n->name : NULL), _node(n) { #ifdef MUOPT.DEBUG cerr << "MuOptDeclError::MuOptDeclError(error_decl*)\n"; #endif } MuOptDeclError: :"MuOptDeclErrorO { } void MuOptDeclError::displayTree(ostream& out, uint indent) const { 68 Sifdef MUOPT.DEBUG cerr << "MuOptDeclError:: displayTree (int) const\n"; #endif indentLine(out, indent); out << "decl.class is Error .decl V " << name() << "\"\n"; } ScopeSet *MuOptDeclError::deps(uint reqNum = 0) const { return new ScopeSet; } A.2.3 mu_opt_expr.cc // mu_opt_expr.cc -*- C++ -*-((include "mu.opt.expr .h" MuOptExpr::MuOptExpr(expr *e) : _node(e), .used(NULL) { #ifdef MUOPT.DEBUG cerr « "MuOptExpr::MuOptExpr(expr*)\n"; #endif _used = new MuOptSTEChain(_node ? _node->used_stes() : NULL); assert(.used); } MuOptExpr::"MuOptExpr() { / /delete .used; } void MuOptExpr::displayTree(ostreamft out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptExpr::displayTree(int) const\n"; #endif indentLine(out, indent); out << "[expr]\n"; _used->displayTree(out, indent + 1); } ScopeSet *MuOptExpr::deps(uint reqNum = 0) const { #ifdef MUOPT.DEBUG cerr « "MuOptExpr::deps(uint=0)\n"; #endif ScopeSet *result; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = _used->deps(reqNum); //cout << "Expr::deps():"; litor(ScopeSet::const.iterator i=result->begin(); i!=result->end(); i++) / / cout << " " << * i ; //cout « "\n"; 69 return result; } MuOptDesignator::"MuOptDesignator() { } MuOptDesignator *MuOptDesignator::newMuOptDesignator(designator *d) { i f ( ! d I I d->left) / / l i s t return new MuOptDesignatorList(d); else / / not a l i s t return new MuOptDesignatorlnstance(d); } MuOptDesignatorInstance::MuOptDesignatorInstance(designator *d) : MuOptExpr(d), _origin(d->origin), .arrayref(d->arrayref), _f ie ldref (d->f ieldref) { #ifdef MUOPT.DEBUG cerr<<"MuOptDesignatorInstance::MuOptDesignatorInstance(designator*)\n"; #endif } MuOptDesignatorInstan.ee : : "MuOptDesignatorInstanceO { > bool MuOptDesignatorlnstance:: i s L i s t O const { return false; } void MuOptDesignatorlnstance::displayTree(ostreamfe out, uint indent) const{ MuOptExpr::displayTree(out, indent); } ScopeSet *MuOptDesignatorInstance::deps(uint reqNum = 0) const { #ifdef MUOPT.DEBUG cerr << "MuOptDesignatorlnstance::deps(uint=0)\n"; #endif ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = MuOptExpr::deps(reqNum); temp = .origin.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; temp = .arrayref.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; temp = _fieldref.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; 70 return result; } MuOptExprList::MuOptExprList(exprlist *e) { #ifdef MUOPT.DEBUG cerr << "MuOptExprList::MuOptExprList(exprlist*)\n"; #endif while(e) { if(e->e) { MuOptExpr *n = new MuOptExpr(e->e); if(n) . l i s t .push.back(n) ; } e = e->next; MuOptExprList::"MuOptExprList() { while(! . l ist .empty()) { / /delete . l i s t . frontO ; . l i s t .pop . f ront ( ) ; > > void MuOptExprList: :displayTree(ostream8: out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptExprList::displayTree(int) const\n"; #endif indentLine(out, indent); out « " [exprlist]\n"; for(list<MuOptExpr*>::const.iterator i=_list .beginO;i!=_list .end();i++) (*i)->displayTree(out, indent + 1); > ScopeSet *MuOptExprList::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = new ScopeSet; for(list<MuOptExpr*>::const.iterator i=_list.beginO;i!=_list.end();i++){ temp = (*i)->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; } return result; MuOptDesignatorList::MuOptDesignatorList(designator *d) { #ifdef MUOPT.DEBUG cerr << "MuOptDesignatorList::MuOptDesignatorList(designator*)\n"; #endif assert(d); while(d) { 71 MuOptDesignatorlnstance *newdesig = new MuOptDesignatorlnstance(d); assert(newdesig); _list.push_back(newdesig); d = d->left; > } MuOptDesignatorList::"MuOptDesignatorList() { while(!_list.empty()) { delete _ l i s t . frontO ; _l ist .pop_front(); } } bool MuOptDesignatorList::isList() const { return true; > void MuOptDesignatorList::displayTree(ostream& out, uint indent) const #ifdef MUOPT.DEBUG cerr << "MuOptDesignatorList: :displayTree(ostream8t,uint) const\n"; #endif //indentLine(indent - 1); / /out << "[designator l i s t ] \n"; for(list<MuOptDesignator!nstance*>::const_iterator i=_l i s t .beginO; i!=_list.end(); i++) (*i)->displayTree(out, indent); } ScopeSet *MuOptDesignatorList::deps(uint reqNum = 0) const { #ifdef MUOPT.DEBUG cerr « "MuOptDesignatorList::deps(uint=0) const\n"; #endif ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = new ScopeSet; for(list<MuOptDesignatorInstance*>::const_iterator i=_l i s t .beginO; i!=_list.end(); i++) { temp = (*i)->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; } return result; } A.2.4 mu_opt_param.cc // mu_opt_param.cc -*- C++ -*-72 #include nmu_opt_param.h" map<param*.MuOptParam*> MuOptParam::_existing; MuOptParam::MuOptParam(Type t , const char *name) : MuOptDecl(Param, name), _type(t) { (tifdef MUOPT.DEBUG cerr << "MuOptParam::MuOptParam(Type, const char*)\n"; #endif } MuOptParam::"MuOptParam() { } void MuOptParam::displayTree(ostream& out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptParam::displayTree(int) const\n"; (tendif indentLine(out, indent); out << "decl.class is Param V " << nameO << "\"\n"; } MuOptParam *MuOptParam: :newMuOptParam(param *p) { MuOptParam *result = NULL; if(p) i f ( .exist ing. f ind(p) == .existing.end()) { switch(p->getparamclass()) { case param::Value: result = new MuOptParamValue(dynamic_cast<valparam*>(p)); break; case param::Var: result = new MuOptParamVar(dynamic_cast<varparam*>(p)); break; case param::Const: result = new MuOptParamConst(dynamic_cast<constparam*>(p)); break; case param::Name: assert(0); / / these don't actually exist in Murphi 3.1!?! / / resu l t = new MuOptParamName(dynamic_cast<nameparam*>(p)); break; case param::Error.param: result = new MuOptParamError(p); break; default: assert(O); break; } .existing[p] = result; } else { result = _existing[p]; (tifdef MUOPT.DEBUG cerr « "reissuing existing param\n"; tendif } return result; } 73 MuOptParamValue::MuOptParamValue(valparam *n) : MuOptParam(Value, n ? n->name : NULL), _node(n) { #ifdef MUOPT.DEBUG cerr << "MuOptParamValue::MuOptParamValue(valparam*)\n"; #endif } MuOptParamValue::"MuOptParamValue() { } void MuOptParamValue::displayTree(ostream& out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptParamValue::displayTree(int) const\n"; (tendif MuOptParam::displayTree(out, indent); indentLine(out, indent + 1); out << "param.class is Value\n"; } ScopeSet *MuOptParamValue::deps(uint reqNum = 0) const { return new ScopeSet; } MuOptParamVar::MuOptParamVar(varparam *n) : MuOptParam(Var, n ? n->name : NULL), _node(n) { (tifdef MUOPT.DEBUG cerr << "MuOptParamVar::MuOptParamVar(varparam*)\n"; #endif } MuOptParamVar::"MuOptParamVar() { } void MuOptParamVar::displayTree(ostreamfe out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptParamVar::displayTree(int) const\n"; (tendif MuOptParam::displayTree(out, indent); indentLine(out, indent + 1); out << "param.class is Var\n"; } ScopeSet *MuOptParamVar::deps(uint reqNum = 0) const { return new ScopeSet; } MuOptParamConst::MuOptParamConst(constparam *n) : MuOptParam(Const, n ? n->name : NULL), _node(n) •( #ifdef MUOPT.DEBUG cerr << "MuOptParamConst::MuOptParamConst(constparam*)\n"; ftendif } MuOptParamConst::"MuOptParamConst() { } void MuOptParamConst::displayTree(ostreamft out, uint indent) const { (tifdef MUOPT.DEBUG 74 cerr << "HuOptParamConst::displayTree(int) const\n"; tendif MuOptParam::displayTree(out, indent); indentLine(out, indent + 1); out << "param_class is Const\n"; } ScopeSet *MuOptParamConst::deps(uint reqNum = 0) const { return new ScopeSet; } /* MuOptParamName::MuOptParamName(nameparam *n) : MuOptParam(Name, n ? n->name : NULL), _node(n) { (tifdef MUOPT.DEBUG cerr << "MuOptParamName::MuOptParamName(nameparam*)\n"; (tendif } MuOptParamName::"MuOptParamName() { } void MuOptParamName::displayTree(ostreamft out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptParamName::displayTree(int) const\n"; tendif MuOptParam::displayTree(out, indent); indentLine(out, indent + 1); out << "param.class is Name\n"; } ScopeSet *MuOptParamName::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = . deps (reqNum) ; temp = .deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; } */ MuOptParamError::MuOptParamError(param *n) : MuOptParam(Error, n ? n->name : NULL), _node(n) { t i fdef MUOPT.DEBUG cerr << "MuOptParamError::MuOptParamError(param*)\n"; tendif } MuOptParamError::"MuOptParamError() { 75 } void MuOptParamError::displayTree(ostream_ out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptParamError::displayTree(int) const\n"; #endif MuOptParam::displayTree(out, indent); indentLine(out, indent +1); out << "param.class is Error\n"; > ScopeSet *MuOptParamError::deps(uint reqNum = 0) const { return new ScopeSet; } A.2.5 mu_opt_root.ee // mu_opt_root.cc -*- C++ -*-#include "mu.opt.root.h" #include <fstream.h> MuOptRoot::MuOptRoot(program *p) : _prog(p), .globals(NULL), .procedures(NULL), .rules(NULL) { #ifdef MUOPT.DEBUG cerr << "MuOptRoot::MuOptRoot(program*)\n"; #endif if(_prog) { .globals = new MuOptSTEChain(_prog->globals); .procedures = new MuOptSTEChain(_prog->procedures, _prog->globals); .rules = new MuOptRuleList(_prog->rules); } } MuOptRoot::"MuOptRoot() { delete .globals; delete .procedures; delete . ru les ; } void MuOptRoot::displayTree(ostreamfe out = cout) const { i f( .prog) { out « "Globals:\n"; _globals->displayTree(out, 1); out << "\nProcedures:\n"; _procedures->displayTree(out, 1); out « "\nRules:\n"; _rules->displayTree(out, 1); } } ScopeSet *MuOptRoot::deps() const { ScopeSet *result, *temp; uint reqNum = MuOptObject: inextReqNumO ; result = _globals->deps(reqNum); 76 temp = _procedures->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; temp = _rules->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; } void MuOptRoot::optimize() { OptRet or; / / before snapshot /*{ ofstream before("/tmp/before"); assert(before.is_open()); displayTree(before); }*/ / / hack some manipulations cout << "Optimizing rules\n"; i f ( . ru les ) { or = _rules->optimize(); assert(or.node == NULL); / / i f (or.node) / / _prog->rules = static_cast<rule*>(or.node); assert(or.obj == NULL); //*+*+* //if(dynamic_cast<MuOptRuleList*>(or.obj)) / / . r u l e s = dynamic_cast<MuOptRuleList>(or.obj); } / / Now, because the parse tree isn't actually used for rule / / generation, we get to rebuild a l l sorts of other data structures / / they are using from our hacked parse tree. (I guess somewhere / / along the way someone didn't understand that optimizations were / / supposed to go in between parsing and code generation, so they / / just hacked their nifty idea for an optimization into the parsing / / stage.) simplerule::SimpleRuleList = NULL; _rules->rebuildRuleInfo(NULL); cout << "Optimization complete\n"; / / now that I'm not bothering to update the parse tree (since Murphi / / ignores i t ) there isn't any point in doing the rebuild after / / clean up and rebuild tree / /delete _globals; / /delete .procedures; / /delete _rules; / / i f (_prog) { / / .globals = new MuOptSTEChain(_prog->globals); / / .procedures = new MuOptSTEChain(_prog->procedures, _prog->globals); / / .rules = new MuOptRuleList(_prog->rules); 77 //} / / after snapshot /*{ ofstream after("/tmp/after"); assert(after.is_open()); displayTree(after); }*/ } A.2.6 mu_opt_rule.cc / / mu_opt_rule . cc - * - C++ - * -tinclude "mu_opt_rule.h" #include <typeinfo> MuOptRuleBase : : "MuOptRuleBaseQ { } MuOptRule : : "MuOptRule ( ) { } bool MuOptRule::isList() const { return false; } MuOptRule *MuOptRule::newMuOptRule(rule *r) { MuOptRule *result = NULL; i f ( r ) switch(r->getclass()) •( case rule: Simple: result = new MuOptRuleSimple(dynamic_cast<simplerule*>(r)); break; case rule: Startstate: result = new MuOptRuleStartstate(dynamic_cast<startstate*>( break; case rule: Invar: result = new MuOptRuleInvar(dynamic_cast<invariant*>(r)); break; case rule: Quant: result - new MuOptRuleQuant(dynamic_cast<quantrule*>(r)); break; case rule: Choose: result = new MuOptRuleChoose(dynamic_cast<chooserule*>(r)); break; i case rule: Alias: result - new MuOptRuleAlias(dynamic_cast<aliasrule*>(r)); break; case rule: Fa ir : result = new MuOptRuleFair(dynamic_cast<fairness*>(r)); break; case rule: Live: result = new MuOptRuleLive(dynamic_cast<liveness*>(r)); break; default: assert(O); } 78 return result; > MuOptRule *MuOptRule::newMuOptRule(MuOptRule *r) { MuOptRule *result = NULL; i f (r) if(typeid(*r) == typeid(MuOptRuleSimple)) result = new MuOptRuleSimple(*dynamic_cast<MuOptRuleSimple*>(r)); else if(typeid(*r) == typeid(MuOptRuleStartstate)) result = new MuOptRuleStartstate(*dynamic_cast<MuOptRuleStartstate*> (r)); else if(typeid(*r) == typeid(MuOptRulelnvar)) result = new MuOptRuleInvar(*dynamic_cast<MuOptRuleInvar*>(r)); else if(typeid(*r) == typeid(MuOptRuleQuant)) result = new MuOptRuleQuant(*dynamic_cast<MuOptRuleQuant*>(r)); else if(typeid(*r) == typeid(MuOptRuleChoose)) result = new MuOptRuleChoose(*dynamic_cast<MuOptRuleChoose*>(r)); else if(typeid(*r) == typeid(MuOptRuleAlias)) result = new MuOptRuleAlias(*dynamic_cast<MuOptRuleAlias*>(r)); else if(typeid(*r) == typeid(MuOptRuleFair)) result = new MuOptRuleFair(*dynamic_cast<MuOptRuleFair*>(r)); else if(typeid(*r) == typeid(MuOptRuleLive)) result = new MuOptRuleLive(*dynamic_cast<MuOptRuleLive*>(r)); else assert(0); return result; } MuOptRuleSimple::MuOptRuleSimple(simplerule *n) : MuOptRule(Simple, n ? n->name : NULL, n), _enclosures(n ? n->enclosures : NULL), _condition(n ? n->condition ; NULL), _locals(n ? n->locals : NULL), _body(n ? n->body : NULL), _unfair(n ? n->unfair : false) { #ifdef MUOPT.DEBUG cerr << "MuOptRuleSimple::MuOptRuleSimple(simplerule*)\n"; tendif } MuOptRuleSimple::MuOptRuleSimple(simplerule*n, Type _type) : MuOptRule(.type, n ? n->name : NULL, n), _enclosures(n ? n->enclosures : NULL), _condition(n &6 _type!=Startstate ? n->condition : NULL), _locals(n && _type!=Invar ? n->locals : NULL), _body(n && _type!=Invar ? n->body : NULL), _unfair(n ? n->unfair : false) { } MuOptRuleSimple::"MuOptRuleSimple() { } const char *MuOptRuleSimple::typeName() const i return "Simple"; } void MuOptRuleSimple::rebuildRuleInfo(const ScopeSet *encl) { t i fdef MUOPT.DEBUG cerr << "MuOptRule" << typeNameO << "::rebuildRuleInfo(const ScopeSet*)\n"; tendif 79 simplerule *n = dynamic_cast<simplerule*>(node()); assert(n); / / update simplerule::SimpleRuleList n->NextSimpleRule = simplerule::SimpleRuleList; simplerule::SimpleRuleList = n; / / update enclosures of this simplerule list<MuOptSTE*>& chain = .enclosures.chainQ; / / HACK: u n z i i i i p . . . i f(encl) { / / This is my second attempt (see CVS rev 1.10 for previous / / version, commented out). This is a bi t ugly, but i t should do. ste *last = NULL; ste *cur = n->enclosures; while (cur) {. II HACK: global scope is hardcoded to 1 / / HACK++: don't throw out scope 0 either if(cur->scope > 1 && encl->find(cur->scope) == enel->end()) { cout << "cleanup: rule \"" << nameO << "\" removing unused enclosing scope " << cur->scope << " from simple rule deps\n"; cur = cur->next; i f ( las t ) last->next = cur; else n->enclosures = cur; } else { last = cur; cur = cur->next; } } MuOptSTEChain temp(n->enclosures); chain.clear(); chain, splice (chain, end () , temp. chainO) ; } else { n->enclosures = NULL; chain.clear(); } / / now that the enclosures have been updated, update the hardcoded / / size parameter so that the magic loop constants work / / <rant>Why is this put into a variable???? If they have a / / b u i l t - i n method to compute i t , why not just c a l l the damn method / / in cpp.code.C rather than using the variable??? Public variables / / are e v i l and should never be used except under very extraordinary / / circumstances, and then only with great care.</rant> / / W e also need to update the indep_card parameter. In theory, i f / / I've optimized things correctly, the new indep.card should always / / b e 1. (I have no idea why asking the appropriate Murphi code to / / recompute i t doesn't come up with 1, but maybe this w i l l become / / clear to me in time.) int newsize = n->CountSize(n->enclosures); if(newsize != n->size I I n->indep_card != 1) { cout « "cleanup: updating magic loop constants for rule \"" « nameO « "\"\n"; n->size = newsize; n->indep_card = 1; } 80 } void MuOptRuleSimple::displayTree(ostream& out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptRule" << typeNameO << ":rdisplayTree(int) const\n"; (tendif indentLine(out, indent); out << "ruleclass is " << typeNameO; if(name()) out « " (" « nameO « ")"; out << "\n"; ihdentLine(out, indent + 1); out << "enclosures\n"; .enclosures.displayTree(out, indent + 2); if(type() != Startstate) { indentLine(out, indent + 1); out << "condition\n"; .condition.displayTree(out, indent + 2); } if(type() != Invar) { indentLine(out, indent + 1); out << "locals\n"; . locals.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "body\n"; .body.displayTree(out, indent + 2); } i f ( .unfa ir ) { indentLine(out, indent + 1); out << "unfair\n"; } ScopeSet *MuOptRuleSimple::deps(uint reqNum = 0) const { (tifdef MUOPT.DEBUG cerr << "MuOptRule" « typeNameO « "::deps(uint=0) const\n"; (tendif ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; result = new ScopeSet; if(depLoop(reqNum)) return result; / / HACK: these conditions on typeO are ugly, should polymorph if(type() != Startstate) { temp = .condition.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; } / / HACK: these conditions on typeO are ugly, should polymorph if(type() != Invar) { temp = .locals.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; 81 temp = .body.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; } return result; } MuOptRuleStartstate::MuOptRuleStartstate(startstate *n) : MuOptRuleSimple(dynamic_cast<simplerule*>(n), Startstate) { #ifdef MUOPT.DEBUG cerr << "MuOptRuleStartstate::MuOptRuleStartstate(simplerule*)\: tendif } MuOptRuleStartstate::"MuOptRuleStartstate() { } const char *MuOptRuleStartstate::typeName() const { return "Startstate"; } MuOptRulelnvar::MuOptRuleInvar(invariant *n) : MuOptRuleSimple(dynamic_cast<simplerule*>(n), Invar) { t i fdef MUOPT.DEBUG cerr << "MuOptRulelnvar::MuOptRuleInvar(simplerule*)\n"; tendif } MuOptRulelnvar:: "MuOptRulelnvarO { } const char *MuOptRuleInvar::typeName() const { return "Invar"; } MuOptRuleQuant::MuOptRuleQuant(quantrule *n) : MuOptRule(Quant, (n && n->quant && n->quant->name ? n->quant->name->getname() : NULL), n), _quant(n ? n->quant : NULL), .rules(NULL) { t i fdef MUOPT.DEBUG cerr « "MuOptRuleQuant::MuOptRuledQuant(quantrule*)\n"; tendif .rules = new MuOptRuleList(n ? n->rules : NULL); assert( .rules); } MuOptRuleQuant::"MuOptRuleQuant() { / /delete .rules; } void MuOptRuleQuant::rebuildRulelnfo(const ScopeSet *encl) { t i fdef MUOPT.DEBUG cerr << "MuOptRuleQuant::rebuildRuleInfo(const ScopeSet*)\n"; tendif ScopeSet newencl; i f (encl) newencl.insert(encl->begin(), encl->end()); newencl. insert (scopeO) ; _rules->rebuildRuleInf o(8tnewencl); 82 } void MuOptRuleQuant::displayTree(ostream& out, uint indent) const (tifdef MUOPT.DEBUG cerr << "MuOptRuleQuant::displayTree(int) const\n"; (tendif indentLine(out, indent); out << "ruleclass is Quant\n"; indentLine(out, indent + 1); out << "quant\n"; .quant.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "rules\n"; _rules->displayTree(out, indent + 2); } ScopeSet *MuOptRuleQuant::deps(uint reqNum = 0) const { (tifdef MUOPT.DEBUG cerr << "MuOptRuleQuant::deps(uint=0) const\n"; (tendif ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = .quant.deps(reqNum); temp = _rules->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; } OptRet MuOptRuleQuant;:optimizeO { (tifdef MUOPT.DEBUG cerr << "MuOptRuleQuant::optimizeO\n"; (tendif OptRet result , rtmp; ScopeSet *temp; result.node = NULL; result .obj = NULL; / / i f .rules is a l i s t , turn me into a l i s t containing multiple / / quant rules with only a single rule in each of their .rules do { i f(_rules->isList()) { int size = dynamic_cast<MuOptRuleList*>(_rules)->size(); cout << "pseudo-opt: ruleset \"" << nameO << "\" (scope « scopeO « ") "; i f ( s ize > 1) cout << "dividing into " << size << " branches\n"; else cout << "rules l i s t has single member, extracting\n"; MuOptRuleList *newlist = new MuOptRuleList(); 83 assert(newlist); MuOptRule *car; MuOptRuleList *cdr = dynamic_cast<MuOptRuleList*>(_rules); assert(cdr); while(cdr) { cdr->split(car, cdr); if(car) { / / SLOPPY MuOptRuleQuant *twin = new MuOptRuleQuant(*this); twin->_rules = car; rtmp = twin->optimize(); if(rtmp.obj != NULL) if(dynamic_cast<MuOptRule*>(rtmp.obj)) newlist->append(dynamic_cast<MuOptRule*>(rtmp.obj)); else if(dynamic_cast<MuOptRuleList*>(rtmp.obj)) newlist->append(dynamic_cast<MuOptRuleList*>(rtmp.obj)) else assert(O); else newlist->append(twin); > > result.node = NULL; result .obj = newlist; return result; } else { rtmp = _rules->optimize(); if(rtmp.obj != NULL) if(dynamic_cast<MuOptRuleBase*>(rtmp.obj)) .rules = dynamic_cast<MuOptRuleBase*>(rtmp.obj); else assert(O); } } while(_rules->isList()); / / i f remaining rule is not dependent on us, commit suicide temp = _rules->deps(); if(temp->find(scopeO) == temp->end()) { cout « "optimization: ruleset \"" « nameO « "\" (scope " << scopeO << ") with no dependencies, removing\n"; / / delete myself MuOptRule *myrule = dynamic_cast<MuOptRule*>(_rules); if(myrule) { result.node = myrule->node(); resuit.obj = myrule; } } return result; MuOptRuleChoose::MuOptRuleChoose(chooserule *n) : MuOptRule(Choose, (n && n->index && n->index->name ? n->index->name->getname() : NULL), n), _index(n ? n->index : NULL), _set(NULL), .rules(NULL) { #ifdef MUOPT.DEBUG cerr << "MuOptRuleChoose::MuOptRuledChoose(chooserule*)\n"; #endif _set = MuOptDesignator::newMuOptDesignator(n ? n->set : NULL); assert(_set); 84 _rul.es = new MuOptRuleList(n ? n->rules : NULL); assert(_rules); } MuOptRuleChoose::"MuOptRuleChoose() { / /delete _rules; } void MuOptRuleChoose::displayTree(ostream_ out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptRuleChoose:: displayTree(int) const\n"; tendif indentLine(out, indent); out << "ruleclass is Choose\n"; indentLine(out, indent + 1); out << " index\n"; _index.displayTree(out, indent + 2); indentLine(out, indent + 1); out « "set\n"; _set->displayTree(out, indent + 2); indentLine(out, indent + 1); out << "rules\n"; _rules->displayTree(out, indent + 2); > ScopeSet *MuOptRuleChoose::deps(uint reqNum = 0) const { #ifdef MUOPT.DEBUG cerr « "MuOptRuleChoose::deps(uint=0) const\n"; #endif ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = .index.deps(reqNum); temp = _set->deps(reqNum); * result->insert(temp->begin(), temp->end()); delete temp; temp = _rules->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; } void MuOptRuleChoose::rebuildRulelnfo(const ScopeSet *encl) { #ifdef MUOPT.DEBUG cerr << "MuOptRuleChoose:rrebuildRulelnfo(const ScopeSet*)\n"; Sendif ScopeSet newencl; i f(encl) newencl.insert(encl->begin(), encl->end()); newencl.insert(scope()); _rules->rebuildRuleInfo(fenewencl); } 85 OptRet MuOptRuleChoose::optimize() { t i fdef MUOPT.DEBUG cerr << "MuOptRuleChoose::rebuildRulelnfo(const ScopeSet*)\n"; #endif OptRet result , rtmp; ScopeSet *temp; result.node = NULL; result .obj = NULL; / / i f .rules is a l i s t , turn me into a l i s t containing multiple / / choose rules with only a single rule in each of their .rules do { i f (_rules->isList()) { int size = dynamic_cast<MuOptRuleList*>(_rules)->size(); cout << "pseudo-opt: choose V " << nameO << "\" (scope " << scopeO << ") "; i f ( s ize > 1) cout << "dividing into " << size << " branches\n"; else cout << "rules l i s t has single member, extracting\n"; MuOptRuleList *newlist = new MuOptRuleListO ; assert(newlist); MuOptRule *car; MuOptRuleList *cdr = dynamic_cast<MuOptRuleList*>(_rules); assert(cdr); while(cdr) { cdr->split(car, cdr); i f (car) { / / SLOPPY MuOptRuleChoose *twin = new MuOptRuleChoose(*this); twin->_rules = car; rtmp = twin->optimize(); if(rtmp.obj != NULL) if(dynamic_cast<MuOptRule*>(rtmp.obj)) newlist->append(dynamic_cast<MuOptRule*>(rtmp.obj)); else if(dynamic_cast<MuOptRuleList*>(rtmp.obj)) newlist->append(dynamic_cast<MuOptRuleList*>(rtmp.obj)); else assert(O); else newlist->append(twin); } } resuit.node = NULL; result .obj = newlist; return result; } else { rtmp = _rules->optimize(); if(rtmp.obj != NULL) if(dynamic_cast<MuOptRuleBase*>(rtmp.obj)) .rules = dynamic_cast<MuOptRuleBase*>(rtmp.obj); else a s s e r t (0 ) ; } } while(_rules->isList()); / / i f remaining rule is not dependent on us, commit suicide temp = _rules->deps(); if(temp->find(scopeO) == temp->end()) { 86 cout << "optimization: choose \"" << name() << "\" (scope " << scopeO << ") with no dependencies, removing\n"; / / delete myself MuOptRule *myrule = dynamic_cast<MuOptRule*>(_rules); if(myrule) { result.node = myrule->node(); result .obj = myrule; } } return result; MuOptRuleAlias::MuOptRuleAlias(aliasrule *n) : MuOptRule (Alias , (n kb. n->aliases _& n->aliases->name ? n->aliases->name->getname() : NULL), n), .al iases(n ? n->aliases : NULL), .rules(NULL) { (tifdef MUOPT.DEBUG cerr << "MuOptRuleAlias::MuOptRuleAlias(aliasrule*)\n"; (tendif .rules = new MuOptRuleList(n ? n->rules : NULL); assert( .rules); } MuOptRuleAlias::"MuOptRuleAlias() { / /delete .rules; } void MuOptRuleAlias::rebuildRuleInfo(const ScopeSet *encl) { (tifdef MUOPT.DEBUG cerr << "MuOptRuleAlias::rebuildRuleInfo(const ScopeSet*)\n"; tendif ScopeSet newencl; i f(encl) newencl.insert(encl->begin(), encl->end()); newencl.insert(.aliases.scope()); _rules->rebuildRuleInfo(ftnewencl); } void MuOptRuleAlias::displayTree(ostream_ out, uint indent) const t i fdef MUOPT.DEBUG cerr << "MuOptRuleAlias::displayTree(int) constSn"; tendif indentLine(out, indent); out << "ruleclass is Al ias\n"; indentLine(out, indent + 1); out << "aliases\n"; .aliases.displayTree(out, indent + 2); indentLine(out, indent + 1); out « "rules\n"; _rules->displayTree(out, indent + 2); } ScopeSet *MuOptRuleAlias::deps(uint reqNum = 0) const { t i fdef MUOPT.DEBUG cerr << "MuOptRuleAlias::deps(uint=0) const\n"; tendif ScopeSet *result, *temp; 87 if(reqNum == 0) reqNum = nextReqNumO ; i f (depLoop(reqNum) ) return new ScopeSet; result = _aliases.deps(reqNum); temp = _rules->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; OptRet MuOptRuleAlias::optimize() { #ifdef MUOPT.DEBUG cerr << "MuOptRuleAlias::optimize()\n"; (tendif OptRet result , rtmp; ScopeSet *temp; result.node = NULL; result .obj = NULL; / / i f .rules is a l i s t , turn me into a l i s t containing multiple / / al ias rules with only a single rule in each of their .rules do { i f (_rules->isList()) { int size = dynamic_cast<MuOptRuleList*>(_rules)->size(); cout << "pseudo-opt: al ias V " << nameO << "\" (scope " « scopeO « ") "; i f ( s ize > 1) cout « "dividing into " « size « " branches\n"; else cout << "rules l i s t has single member, extracting\n"; MuOptRuleList *newlist = new MuOptRuleList(); assert(newlist); MuOptRule *car; MuOptRuleList *cdr = dynamic_cast<MuOptRuleList*>(.rules); assert(cdr); while(cdr) { cdr->split(car, cdr); i f (car) { MuOptRuleAlias *twin = new MuOptRuleAlias(*this); twin->_rules = car; rtmp = twin->optimize(); if(rtmp.obj != NULL) if(dynamic_cast<MuOptRule*>(rtmp.obj)) newlist->append(dynamic_cast<MuOptRule*>(rtmp.obj)); else if(dynamic_cast<MuOptRuleList*>(rtmp.obj)) newlist->append(dynamic_cast<MuOptRuleList*>(rtmp.obj)); else assert(O); else newlist->append(twin); } } result , node = NULL; result .obj = newlist; 88 return result; } else { rtmp = _rules->optimize(); if(rtmp.obj != NULL) if(dynamic_cast<MuOptRuleBase*>(rtmp.obj)) _rules = dynamic_cast<MuOptRuleBase*>(rtmp.obj); else assert(O); } } while(_rules->isList()); / / i f remaining rule is not dependent on us, commit suicide temp = _rules->deps(); if(temp->find(scope()) == temp->end()) { cout << "optimization: al ias V " << nameO << "\" (scope " << scopeO << ") with no dependencies, removing\n"; / / delete myself MuOptRule *myrule = dynamic_cast<MuOptRule*>(.rules); if(myrule) { result.node = myrule->node(); result.obj = myrule; } } return result; } MuOptRuleFair::MuOptRuleFair(fairness *n) : MuOptRule(Fair, n ? n->name : NULL, n) { #ifdef MUOPT.DEBUG cerr << "MuOptRuleFair::MuOptRuledFair(fairness*)\n"; #endif assert(0); } MuOptRuleFair::"MuOptRuleFair() { } void MuOptRuleFair::displayTree(ostreamft out, uint indent) const #ifdef MUOPT.DEBUG cerr << "MuOptRuleFair::displayTree(int) const\n"; #endif } ScopeSet *MuOptRuleFair::deps(uint reqNum = 0) const { #ifdef MUOPT.DEBUG cerr << "MuOptRuleFair::deps(uint=0) const\n"; #endif assert(0); return NULL; / * ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; 8 9 result = .deps(reqNum); temp = .deps(reqNum); result->insert(terap->begin(), temp->end()); delete temp; return result; void HuOptRuleFair::rebuildRulelnfo(const ScopeSet *encl) { assert(0); } MuOptRuleLive::MuOptRuleLive(liveness *n) : MuOptRule(Live, n ? n->name : NULL, n) { #ifdef MUOPT.DEBUG cerr << "MuOptRuleLive::MuOptRuledLive(liveness*)\n"; #endif assert(0); > MuOptRuleLive::"MuOptRuleLive() { } void MuOptRuleLive::displayTree(ostreamft out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptRuleLive::displayTree(int) const\n"; tendif } ScopeSet *MuOptRuleLive::deps(uint reqNum = 0) const { t i fdef MUOPT.DEBUG cerr << "MuOptRuleLive::deps(uint=0) const\n"; tendif assert(O); return NULL; / * ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumQ ; if(depLoop(reqNum)) return new ScopeSet; result = .deps(reqNum); temp = .deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; * / } void MuOptRuleLive::rebuildRulelnfo(const ScopeSet *encl) -[ assert(0); 90 } MuOptRuleList::MuOptRuleList(rule *r) { (tifdef MUOPT.DEBUG cerr « "MuOptRuleList::MuOptRuleList(rule*)\n"; (tendif assert(r); while(r) { MuOptRule *newrule = MuOptRule : :newMuOptRule (r) ; assert(newrule); .list.push.back(newrule); r = r->next; } } MuOptRuleList::MuOptRuleList(const MuOptRuleList *r) { #ifdef MUOPT.DEBUG cerr « "MuOptRuleList::MuOptRuleList(MuOptRuleList*)\n"; #endif i f (r) for(list<MuOptRule*>::const.iterator i = r ->_l i s t .beginO; i != r->_list.end(); i++) . l ist .push_back(*i); } MuOptRuleList::"MuOptRuleList() { while(!. l ist .empty()) { delete . l i s t . f r o n t ( ) ; . l i s t .pop . f ront ( ) ; > } void MuOptRuleList::displayTree(ostreamft out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptRuleLive::displayTree(int) const\n"; (tendif //indentLine(indent - 1); //out « "[rule l i s t ] \n"; for(list<MuOptRule*>::const.iterator i=_list .beginO;i!=_list .end();i++) (*i)->displayTree(out, indent); } ScopeSet *MuOptRuleList::deps(uint reqNum = 0) const { (tifdef MUOPT.DEBUG cerr << "MuOptRuleList::deps(uint=0) const\n"; (tendif ScopeSet *result, *temp; if(reqNum - - 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; result = new ScopeSet; for ( l i s t <MuOptRule*>: : const. iterator i=_list .beginO ; i ! =_list. endO ; i++){ temp = (*i)->deps(reqNum); result->insert(temp->begin(), temp->end()) ; 91 delete temp; return result; } OptRet MuOptRuleList:: optimizeO { t i fdef MUOPT.DEBUG cerr << "MuOptRuleList::optimize()\n"; tendif OptRet result , temp; bool modified = true; resuit.node = NULL; result .obj = NULL; while(modified) { modified = false; list<MuOptRule*> :: iterator i = _ l i s t .beginO ; while(i != _list .end()) { temp = (*i)->optimize(); / / ignore temp.node if(dynamic_cast<MuOptRule*>(temp.obj)) { * i = dynamic_cast<MuOptRule*>(temp.obj); i++; modified = true; } else if(dynamic_cast<MuOptRuleList*>(temp.obj)) { cout « " c l e a n u p : merging generated l i s t with existing l i s t \ MuOptRuleList *sublist = dynamic.cast<MuOptRuleList*>(temp.obj); list<MuOptRule*>::iterator j = i , k = i ; i++; _ l i s t . i n s e r t ( j , subl is t ->_l is t .beginO, sublist->_list .end()); . l i s t . erase (k ) ; modified = true; i = _ l is t .end(); } else if(temp.obj ! = NULL) assert(0); else i++; } } / / i f we only have one chi ld , return the chi ld and delete ourself i f (_list . s i z e O == 1) { cout « "pseudo-opt: single member rule l i s t -> rule\n"; / /result .node = NULL; / / no transformation necessary on the / / / / Murphi tree result .obj = _ l i s t . f ront ( ) ; } return result; } bool MuOptRuleList:: i s L i s t O const { return true; } void MuOptRuleList::rebuildRuleInfo(const ScopeSet *encl) { t i fdef MUOPT.DEBUG cerr << "MuOptRuleList::rebuildRule!nfo(const ScopeSet*)\n"; 92 #endif for(list<MuOptRule*>::const.iterator i=_list.beginO;i!=_list.end();i++) (*i)->rebuildRuleInfo(encl); } void MuOptRuleList::split(MuOptRule*. car, MuOptRuleList*- cdr) const { i f ( - l i s t . s i z e O > 1) { cdr = new MuOptRuleList(this); car = cdr->pop_f rontO ; "} else { cdr = NULL; i f ( _ l i s t . s i z e ( ) == 1) car = - l i s t . f r o n t ( ) ; else car = NULL; } } MuOptRule *MuOptRuleList: :pop_f rontO { i f ( . l i s t . s i z e O > 0) { MuOptRule *result = . l i s t . f r o n t ( ) ; - l i s t .pop- front ( ) ; return result; } else return NULL; } void MuOptRuleList::append(MuOptRule *r) { i f ( r ) - l i s t .push-back(r); } void MuOptRuleList::append(const MuOptRuleList *rl ) { i f ( r l ) - l i s t . i n s e r t ( - l i s t . e n d ( ) , r l - > _ l i s t . b e g i n O , r l ->_l ist .end()); } A.2.7 mu_opt_ste.cc // mu.opt.ste. cc -*- C++ -*-((include "mu.opt.ste.h" ((include "mu.opt.decl .h" MuOptSTE::MuOptSTE(ste *s) : MuOptObject(s ? (s->getname() ? s->getname()->getname() : NULL) :NULL), _node(s), _scope(s ? s->getscope() : -1), _lextype(s ? (s->getname() ? s->getname()->getlextype() : -2) : -1), .value(NULL) { (tifdef MUOPT.DEBUG cerr « "MuOptSTE::MuOptSTE(ste*)\n"; (tendif //assert(_lextype != -1); assert(.lextype != -2); if(.node) { .value = MuOptDecl::newMuOptDecl(_node->getvalue()); assert(.value); 93 } } MuOptSTE::"MuOptSTE() { / /delete _value; } void MuOptSTE::displayTree(ostream_ out, uint indent) const { t i fdef MUOPT.DEBUG cerr << "MuOptSTE::displayTree(int) const\n"; tendif if(.node) { indentLine(out, indent); out << " [ste]"; if(_node->getname()) out « " " « .scope << " : : " « nameO « "(" << .lextype « ")" out << "\n"; i f( .value) { indentLine(out, indent + 1); out << "value\n"; _value->displayTree(out, indent + 2); > } } ScopeSet *MuOptSTE::deps(uint reqNum = 0) const { ScopeSet *result; if(reqNum - - 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; i f ( .value) result = _value->deps(reqNum); else result = new ScopeSet; result->insert (.scope),; return result; } MuOptSTEChain::MuOptSTEChain(ste *start, ste *stop) { #ifdef MUOPT.DEBUG cerr « "MuOptSTEChain::MuOptSTEChain(ste*, ste*)\n"; tendif for(ste * i = start; i &_ i != stop; i = i->next) { MuOptSTE *s = new MuOptSTE(i); assert(s); i f ( s ) .chain.push.back(s); } } MuOptSTEChain::MuOptSTEChain(stelist *start, s te l i s t *stop) { t i fdef MUOPT.DEBUG cerr « "MuOptSTEChain::MuOptSTEChain(stelist*, stelist*)\n"; tendif 94 for(s te l i s t * i = start; i __ i != stop; i = i->next) for(ste *j = i->s; j ; j = j->next) { MuOptSTE *s = new MuOptSTE(j); assert(s); i f (s) .chain.push_back(s); } } MuOptSTEChain::MuOptSTEChain(stecoll *s) { #ifdef MUOPT.DEBUG cerr « "MuOptSTEChain::MuOptSTEChain(stecoll*)\n"; #endif / / The way this one works doesn't make a ton of sense to me, but then / / why have redundant data structures? (Ans: because Murphi is only / / weakly 00, and not at a l l 00 when i t comes to STEs.) i f (s) for(s te l i s t * i = s->first; i ; i = i->next) { MuOptSTE *n = new MuOptSTE(i->s); assert(s) ; if(n) .chain.push.back(n); } } MuOptSTEChain::"MuOptSTEChain() { while(! .chain.emptyO) { / /delete .chain . frontO ; .chain.pop.frontO ; } } void MuOptSTEChain::displayTree(ostream. out, uint indent) const { (tifdef MUOPT.DEBUG cerr « "MuOptSTEChain::displayTree(int) const\n"; tendif for(list<MuOptSTE*>::const.iterator i = .chain.beginO; i != .chain.endO; i++) { (*i)->displayTree(out, indent); } } ScopeSet *MuOptSTEChain::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumQ; if(depLoop(reqNum)) return new ScopeSet; result = new ScopeSet; f orOist<Mu0ptSTE*>:: const. iterator i = .chain.beginO ; i != .chain.endO; i++) { temp = (*i)->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; } return result; 95 } ScopeSet *MuOptSTEChain::scopesO const { ScopeSet *result = new ScopeSet; for(list<MuOptSTE*>::const.iterator i = .chain.beginO; i != .chain.endO; i++) result->insert((*i)->scope()); return result; } A.2.8 mu_opt_stmt.cc / / mu_opt_stmt.cc - * - C++ - * -#include "mu_opt_stmt.h" #include <typeinfo> map<stmt*,MuOptStmt*> MuOptStmt::_existing; MuOptStmt::"MuOptStmt() { } MuOptStmt *MuOptStmt:mewMuOptStmt (stmt *s) { MuOptStmt *result = NULL; i f (s) i f ( .existing.find(s) == .exist ing.endO) { II no getclassO here, so get to use RTTI (woohoo!) if(typeid(*s) == typeid(assignment)) result = new MuOptStmtAssignment(dynamic_cast<assignment*>(s)); else if(typeid(*s) == typeid(whilestmt)) result = new MuOptStmtWhile(dynamic_cast<whilestmt*>(s)); else if(typeid(*s) == typeid(ifstmt)) result = new MuOptStmtlf(dynamic_cast<ifstmt*>(s)); else if(typeid(*s) == typeid(caselist)) result = new MuOptStratCase(dynamic_cast<caselist*>(s)); else if(typeid(*s) == typeid(switchstmt)) result = new MuOptStmtSwitch(dynamic_cast<switchstmt*>(s)); else if(typeid(*s) == typeid(forstmt)) result = new MuOptStmtFor(dynamic_cast<forstmt*>(s)); else if(typeid(*s) == typeid(proccall)) result = new MuOptStmtProc(dynamic_cast<proccall*>(s)); else if(typeid(*s) == typeid(clearstmt)) result = new MuOptStmtClear(dynamic_cast<clearstmt*>(s)); else if(typeid(*s) == typeid(errorstmt)) result = new MuOptStmtError(dynamic_cast<errorstmt*>(s)); else if(typeid(*s) == typeid(assertstmt)) result = new MuOptStmtAssert(dynamic_cast<assertstmt*>(s)); else if(typeid(*s) == typeid(putstmt)) result = new MuOptStmtPut(dynamic_cast<putstmt*>(s)); else if(typeid(*s) == typeid(alias)) result = new MuOptStmtAlias(dynamic_cast<alias*>(s)); else if(typeid(*s) == typeid(aliasstmt)) result = new MuOptStmtAliasstmt(dynamic_cast<aliasstmt*>(s)); 96 else if(typeid(*s) == typeid(returnstmt)) result = new MuOptStmtReturn(dynamic_cast<returnstmt*>(s)); else if(typeid(*s) == typeid(undefinestmt)) / / not on "the l i s t " result = new MuOptStmtUndefine(dynamic_cast<undefinestmt*>(s)); else if(typeid(*s) == typeid(multisetaddstmt)) / / not on "the l i s t" result=new MuOptStmtMultisetAdd(dynamic_cast<multisetaddstmt*>(s)); else if(typeid(*s) == typeid(multisetremovestmt)) / /not on "the l i s t" result = new MuOptStmtMultisetRemove(dynamic_cast<multisetremovestmt*>(s)); else i f ( s == nullstmt) / / have to read carefully to f ind this one result = new MuOptStmtNull(); else assert(O); _existing[s] = result; } else { result = _existing[s]; (tifdef MUOPT.DEBUG cerr << "reissuing existing stmt\n"; (tendif } return result; } MuOptStmtList::MuOptStmtList(stmt *s) { (tifdef MUOPT.DEBUG cerr « "MuOptStmtList::MuOptStmtList(stmt*)\n"; (tendif while(s) { MuOptStmt *mos = MuOptStmt::newMuOptStmt(s); if(mos) .list.push.back(mos); s = s->next; } } MuOptStmtList::"MuOptStmtList() { while(! . l ist .empty()) { / /delete . l i s t . f r o n t ( ) ; . l i s t .pop . f ront ( ) ; } } void MuOptStmtList::displayTree(ostreamft out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptStmtList::displayTree(int) const\n"; (tendif //indentLine(indent - 1); //out « "[stmtlist]\n"; for(list<MuOptStmt*>::const.iterator i=_list .beginO;i!=_list .end();i++) (*i)->displayTree(out, indent); } ScopeSet *MuOptStmtList::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; 97 result = new ScopeSet; for(list<MuOptStmt*>::const.iterator i=_list.beginO;i!=_list.end();i++){ temp = (*i)->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; } return result; } MuOptStmtAssignment::MuOptStmtAssignment(assignment *a) : MuOptStmt(Assignment), _node(a), _src(a ? a->src : NULL), .target(NULL) { #ifdef MUOPT.DEBUG cerr « "MuOptStmtAssignment::MuOptStmtAssignment(assignment*)\n"; #endif assert(a); .target = MuOptDesignator::newMuOptDesignator(a->target); assert(.target); } MuOptStmtAssignment::"MuOptStmtAssignment() { > void MuOptStmtAssignment::displayTree(ostreamfe out, uint indent) const { t i fdef MUOPT.DEBUG cerr << "MuOptStmtAssignment::displayTree(int) const\n"; tendif indentLine(out, indent); out << "assignment\n"; indentLine(out, indent + 1); out << "target\n"; _target->displayTree(out, indent + 2); indentLine(out, indent + 1); out << "src\n"; _src.displayTree(out, indent + 2); } ScopeSet *MuOptStmtAssignment::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO ; if(depLoop(reqNum)) return new ScopeSet; result = _target->deps(reqNum); temp = _src.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; } MuOptStmtWhile::MuOptStmtWhile(whilestmt *w) : MuOptStmt(While), _node(w), .test(w->test), .body(_node->body) { t i fdef MUOPT.DEBUG 98 cerr « "MuOptStmtWhile::MuOptStmtWhile(whilestmt*)\n"; #endif } MuOptStmtWhile: :"MuOptStmtWhileO { } void MuOptStmtWhile::displayTree(ostream_ out, uint indent) const (tifdef MUOPT.DEBUG cerr << "MuOptStmtWhile: : displayTree (int) const\n"; (tendif indentLine(out, indent); out << "whilestmt\n"; indentLine(out, indent + 1); out << "test\n"; .test.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "body\n"; .body.displayTree(out, indent + 2); } ScopeSet *MuOptStmtWhile::deps(uint reqNum = 0 ) const { ScopeSet *result, *temp; if(reqNum == 0 ) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; result = .test.deps(reqNum); temp = .body.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; } MuOptStmtlf::MuOptStmtIf(ifstmt *i) : MuOptStmt(If), _node(i), _test(i->test), .body(i->body), _else(i->elsecode) { (tifdef MUOPT.DEBUG cerr « "MuOptStmtlf::MuOptStmtIf(ifstmt*)\n"; (tendif } MuOptStmtlf::"MuOptStmtlf() { } void MuOptStmtlf::displayTree(ostream& out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptStmtlf::displayTree(int) const\n"; (tendif indentLine(out, indent); out « "ifstmt\n"; indentLine(out, indent + 1); out « "test\n"; .test.displayTree(out, indent + 2); indentLine(out, indent +1); 99 out << "body\n"; .body.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "elsecode\n"; .else.displayTree(out, indent + 2); } ScopeSet *MuOptStmtIf::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumQ ; if(depLoop(reqNum)) return neu ScopeSet; result = .test.deps(reqNum); temp = .body.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; temp = .else.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; } MuOptStmtCase::MuOptStmtCase(caselist *c) : MuOptStmt(Case), _node(c), _values(c->va_ues), .body(c->body) { (tifdef MUOPT.DEBUG cerr « "MuOptStmtCase::MuOptStmtCase(caselist*)\n"; tendif } MuOptStmtCase::"MuOptStmtCase() { > void MuOptStmtCase::displayTree(ostreamft out, uint indent) const { t i fdef MUOPT.DEBUG cerr « "MuOptStmtCase::displayTree(int) const\n"; tendif indentLine(out, indent); out << "case\n"; indentLine(out, indent + 1); out << "values\n"; .values.displayTree(out, indent + 2); indentLine(out, indent + 1); out « "body\n"; .body.displayTree(out, indent + 2); } ScopeSet *MuOptStmtCase::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum ==0) reqNum = nextReqNumQ; if(depLoop(reqNum)) 100 return new ScopeSet; result = _values.deps(reqNum); temp = _body.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; > MuOptStmtCaseList::MuOptStmtCaseList(caselist *c) { #ifdef MUOPT.DEBUG cerr << "MuOptStmtCaseList::MuOptStmtCaseList(caselist*)\n"; #endif while(c) { MuOptStmtCase *mosc = new MuOptStmtCase(c); if(mosc) .list.push_back(mosc); c = c->next; } } MuOptStmtCaseList::"MuOptStmtCaseListO { while(! . l i s t . emptyO) { / /delete . l i s t . f r o n t ( ) ; _l ist .pop_front(); } } void MuOptStmtCaseList::displayTree(ostreamft out, uint indent) const -C t i fdef MUOPT.DEBUG cerr « "MuOptStmtCaseList::displayTree(int) const\n"; tendif for(list<MuOptStmtCase*>::const.iterator i = . l i s t . b e g i n O ; i != . l i s t . e n d O ; i++) (*i)->displayTree(out, indent); } ScopeSet *MuOptStmtCaseList::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; result = new ScopeSet; for(list<MuOptStmtCase*>::const.iterator i = . l i s t . b e g i n O ; i != . l i s t . e n d O ; i++) { temp = (*i)->deps(reqNum); result->insert(temp->begin(), terap->end()); delete temp; } return result; } MuOptStmtSwitch::MuOptStmtSwitch(switchstmt *s) : 101 MuOptStmt(Switch), _node(s), .expr(s->switchexpr), _cases(s->cases), _def ault(s->elsecode) { #ifdef MUOPT.DEBUG cerr << "MuOptStmtSwitch::MuOptStmtSwitch(switchstmt*)\n"; tendif } MuOptStmtSwitch: : "MuOptStmtSwitchO { } void MuOptStmtSwitch::displayTree(ostream_ out, uint indent) const { t i fdef MUOPT.DEBUG cerr « "MuOptStmtSwitch::displayTree(int) const\n"; tendif indentLine(out, indent); out << "switchstmt\n"; indentLine(out, indent + 1); out << "switchexpr\n"; .expr.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "cases\n"; .cases.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "elsecode\n"; .default.displayTree(out, indent + 2); } ScopeSet *MuOptStmtSwitch::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum ==0) reqNum = nextReqNumQ ; if(depLoop(reqNum)) return new ScopeSet; result = .expr.deps(reqNum); temp = .cases.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; temp = .default .deps(reqNum) ; result->insert(temp->begin(), temp->end()); delete temp; return result; } MuOptStmtFor::MuOptStmtFor(forstmt *f) : MuOptStmt(For), _node(f), .index(f->index), .body(f->body) { t i fdef MUOPT.DEBUG cerr << "MuOptStmtFor::MuOptStmtFor(forstmt*)\n"; tendif } MuOptStmtFor::"MuOptStmtFor() { } void MuOptStmtFor::displayTree(ostream. out, uint indent) const { 1 0 2 #ifdef MUOPT.DEBUG cerr << "MuOptStmtFor::displayTree(int) const\n"; #endif indentLine(out, indent); out << "forstmt\n"; indentLine(out, indent + 1); out << "index\n"; .index.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "body\n"; .body.displayTree(out, indent + 2); } ScopeSet *MuOptStmtFor::deps(uint reqNum = 0) const { ScopeSet tresult , *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; result = .index.deps(reqNum); temp = .body, deps (reqNum) ; result->insert(temp->begin(), temp->end()); delete temp; return result; MuOptStmtProc::MuOptStmtProc(proccall *p) : MuOptStmt(Proc), _node(p), _procedure(p->procedure), _actuals(p->actuals) { #ifdef MUOPT.DEBUG cerr « "MuOptStmtProc::MuOptStmtProc(proccall*)\n"; Sendif MuOptStmtProc::"MuOptStmtProc() .{ > void MuOptStmtProc::displayTree(ostreamft out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptStmtProc::displayTree(int) const\n"; Sendif indentLine(out, indent); out « "proccall\n" ; indentLine(out, indent + 1); out << "procedure\n"; .procedure.displayTree(out, indent + 2); indentLine(out, indent + 1); out << "actuals\n"; .actuals.displayTree(out, indent + 2); } ScopeSet *MuOptStmtProc::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) 103 reqNum = nextReqNumQ ; if(depLoop(reqNum)) return new ScopeSet; result = .procedure.deps(reqNum); temp = .actuals.deps(reqNum); resuit->insert(temp->begin(), temp->end()); delete temp; return result; } MuOptStmtClear::MuOptStmtClear(clearstmt *c) : MuOptStmt(Clear), _node(c), .target(NULL) { #ifdef MUOPT.DEBUG cerr << "MuOptStmtClear::MuOptStmtClear(clearstmt*)\n"; tendif assert(c); .target = MuOptDesignator::newMuOptDesignator(c->target); assert( .target); } MuOptStmtClear::"MuOptStmtClear() { / /delete .target; } void MuOptStmtClear::displayTree(ostream. out, uint indent) const { t i fdef MUOPT.DEBUG cerr « "MuOptStmtClear::displayTree(int) const\n"; tendif indentLine(out, indent); out << "clearstmt\n"; indentLine(out, indent + 1); out << "target\n"; _target->displayTree(out, indent + 2 ) ; } ScopeSet *MuOptStmtClear::deps(uint reqNum = 0) const { ScopeSet *resu l t ; / / , *temp; if(reqNum == 0) reqNum = nextReqNumQ; if(depLoop(reqNum)) return new ScopeSet; result = _target->deps(reqNum); /* temp = .deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; */ return result; } MuOptStmtError::MuOptStmtError(errorstmt *c) : 104 MuOptStmt(Error), _node(c), _string(c->string) { t i fdef MUOPT.DEBUG cerr « "MuOptStmtError::MuOptStmtError(errorstmt*)\n"; tendif } MuOptStmtError::MuOptStmtError(errorstmt *c, bool isassert) : MuOptStmt(isassert ? Assert : Error) , _node(c), _string(c->string) { t i fdef MUOPT.DEBUG cerr << "MuOptStmtError::MuOptStmtError(errorstmt*, bool)\n"; tendif } MuOptStmtError::"MuOptStmtError() { } void MuOptStmtError::displayTree(ostreamSfc out, uint indent) const { t i fdef MUOPT.DEBUG cerr << "MuOptStmtError: :displayTree(int) const\n"; tendif indentLine(out, indent); out « "errorstmt V " « . s tr ing « "\"\n"; } ScopeSet *MuOptStmtError::deps(uint reqNum = 0) const { / /assert(O); return new ScopeSet; } MuOptStmtAssert::MuOptStmtAssert(assertstmt *c) : MuOptStmtError(c, true), _node(c), .test(c->test){ t i fdef MUOPT.DEBUG cerr << "MuOptStmtAssert::MuOptStmtAssert(assertstmt*)\n"; tendif } MuOptStmtAssert: :"MuOptStmtAssertO { } void MuOptStmtAssert::displayTree(ostreamft out, uint indent) const -( t i fdef MUOPT.DEBUG cerr << "MuOptStmtAssert:: displayTree (int) const\n"; tendif indentLine(out, indent); out << "assertstmt\n"; indentLine(out, indent + 1); out << "test\n"; .test.displayTree(out, indent + 2); indentLine(out, indent + 1); out « " s t r i n g W ; indentLine(out, indent + 2); out << errs tr ingO « "\n"; } ScopeSet *MuOptStmtAssert::deps(uint reqNum = 0) const { if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; 105 return _test.deps(reqNum); } MuOptStmtPut::MuOptStmtPut(putstmt *c) : MuOptStmt(Put), _node(c) { (tifdef MUOPT.DEBUG cerr << "MuOptStmtPut::MuOptStmtPut(putstmt*)\n"; (tendif assert(O); } MuOptStmtPut::"MuOptStmtPut() { } void MuOptStmtPut: :displayTree(ostreamSt out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptStmtPut::displayTree(int) const\n"; (tendif indentLine(out, indent); out << "putstmt\n"; } ScopeSet *MuOptStmtPut::deps(uint reqNum = 0) const { assert(0); return NULL; / * ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumQ ; if(depLoop(reqNum)) return new ScopeSet; result = .deps(reqNum); temp = .deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; * / } MuOptStmtAlias::MuOptStmtAlias(alias *c) : MuOptStmt(Alias), _node(c) { (tifdef MUOPT.DEBUG cerr « "MuOptStmtAlias::MuOptStmtAlias(alias*)\n"; tendif assert(O); } MuOptStmtAlias::"MuOptStmtAlias() { } void MuOptStmtAlias::displayTree(ostream. out, uint indent) const t i fdef MUOPT.DEBUG cerr << "MuOptStmtAlias::displayTree(int) const\n"; tendif 106 indentLine(out, indent); out << "alias\n"; } ScopeSet *MuOptStmtAlias::deps(uint reqNum = 0 ) const { a s ser t (0 ) ; return NULL; / * ScopeSet *result, *temp; i f (reqNum == 0 ) reqNum = nextReqNumQ ; if(depLoop(reqNum)) return new ScopeSet; result = .deps(reqNum); temp = .deps(reqNum); result->insert (temp->begin() , temp->endQ) ; delete temp; return result; * / } MuOptStmtAliasstmt::MuOptStmtAliasstmt(aliasstmt *a) : MuOptStmt(Aliasstmt), _node(a), _aliases(a->aliases), _body(a->body) { #ifdef MUOPT.DEBUG cerr << "MuOptStmtAliasstmt::MuOptStmtAliasstmt(aliasstmt*)\n"; #endif } MuOptStmtAliasstmt::"MuOptStmtAliasstmt() { } void MuOptStmtAliasstmt::displayTree(ostreamSt out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptAliasstmt::displayTree(int) const\n"; tendif indentLine(out, indent); out << "aliasstmt\n"; indentLine(out, indent + 1 ) ; out << " a l i a s e s W ; .aliases.displayTree(out, indent + 2); indentLine(out, indent + 1); out « "body\n"; .body.displayTree(out, indent + 2); } ScopeSet *MuOptStmtAliasstmt::deps(uint reqNum = 0 ) const { ScopeSet *result, *temp; if(reqNum == 0 ) reqNum = nextReqNumQ; if(depLoop(reqNum)) return new ScopeSet; result = .aliases.deps(reqNum); 107 temp = _body.deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; } MuOptStmtReturn::MuOptStmtReturn(returnstmt *r) : MuOptStmt (Return) , .node(r) , .retexpr (r->retexpr) -( t i fdef MUOPT.DEBUG cerr << "MuOptStmtReturn::MuOptStmtReturn(returnstmt*)\n"; tendif } MuOptStmtReturn: : "MuOptStmtReturnQ { } void MuOptStmtReturn::displayTree(ostream& out, uint indent) const -( t i fdef MUOPT.DEBUG cerr << "MuOptStmtReturn::displayTree(int) const\n"; tendif indentLine(out, indent); out << "returnstmt\n"; indentLine(out, indent + 1); out << "retexpr\n"; _retexpr.displayTree(out, indent +2); } ScopeSet *MuOptStmtReturn::deps(uint reqNum = 0) const { if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; return .retexpr.deps(reqNum); } MuOptStmtUndefine::MuOptStmtUndefine(undefinestmt *u) : MuOptStmt(Undefine), _node(u), .target(NULL) { t i fdef MUOPT.DEBUG cerr « "MuOptStmtUndefine::MuOptStmtUndefine(undefinestmt*)\n"; tendif .target = MuOptDesignator::newMuOptDesignator(u ? u->target : NULL); assert(.target); } MuOptStmtUndef ine::"MuOptStmtUndef ine() { } void MuOptStmtUndefine::displayTree(ostreamft out, uint indent) const { t i fdef MUOPT.DEBUG cerr << "MuOptStmtUndefine::displayTree(int) const\n"; tendif indentLine(out, indent); out << "undefinestmt\n"; _target->displayTree(out, indent + 1); } 108 ScopeSet *MuOptStmtUndefine::deps(uint reqNum = 0) const { ScopeSet *resu l t ; / / , *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; result = _target->deps(reqNum); /* temp = . deps (reqNum) ; result->insert(temp->begin(), temp->end()); delete temp; */ return result; } MuOptStmtMultisetAdd::MuOptStmtMultisetAdd(multisetaddstmt *u) : MuDptStmt(MultisetAdd), _node(u), .element(NULL), .target(NULL) { #ifdef MUOPT.DEBUG cerr « "MuOptStmtMultisetAdd: :MuOptStmtMultisetAdd(multisetaddstmt*)\n" tendif .element = MuOptDesignator::newMuOptDesignator(u ? u->element : NULL); assert(.element); .target = MuOptDesignator::newMuOptDesignator(u ? u->target : NULL); assert( .target); } MuOptStmtMultisetAdd::"MuOptStmtMultisetAddO { } void MuOptStmtMultisetAdd::displayTree(ostream& out, uint indent) const { t i fdef MUOPT.DEBUG cerr « "MuOptMultisetAdd::displayTree(int) const\n"; tendif indentLine(out, indent); out << "multisetaddstmt\n"; indentLine(out, indent + 1); out << "element\n"; _element->displayTree(out, indent + 2); indentLine(out, indent + 1); out « "target\n"; _target->displayTree(out, indent + 2); } ScopeSet *MuOptStmtMultisetAdd::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; result = _element->deps(reqNum); temp = _target->deps(reqNum); 109 result->insert(temp->begin(), temp->end()); delete temp; return result; > MuOptStmtMult isetRemove::MuOptStmtMult isetRemove(mult isetremovestmt *u) : MuOptStmt(Hult i setRemove) , _node(u) , _ index(u ? u->index : NULL), . t a r g e t ( N U L L ) , _ c r i t e r i o n ( u ? u - > c r i t e r i o n : NULL) { # i fdef MUOPT.DEBUG c e r r << "MuOptStmtMultisetRemove::" 11 MuOptStmtMulti set Remove ( m u l t i set removestmt*)\n" ; #endif . t a r g e t = MuOptDesignator::newMuOptDesignator(u ? u->target : NULL); a s s e r t ( . t a r g e t ) ; } MuOptStmtMult isetRemove::"MuOptStmtMult isetRemoveO { / / d e l e t e . t a r g e t ; } v o i d MuOptStmtMultisetRemove: ' .displayTree(ostreamSt out , u i n t indent ) const{ # i fde f MUOPT.DEBUG c e r r << " M u O p t M u l t i s e t R e m o v e : : d i s p l a y T r e e ( i n t ) c o n s t \ n " ; #endif i n d e n t L i n e ( o u t , i n d e n t ) ; out << "mult i se tremovestmt\n"; i n d e n t L i n e ( o u t , indent + 1); out « " index \n"; . i n d e x . d i s p l a y T r e e ( o u t , indent + 2); i n d e n t L i n e ( o u t , indent + 1); out « " t a r g e t \ n " ; _ t a r g e t - > d i s p l a y T r e e ( o u t , indent + 2); i n d e n t L i n e ( o u t , indent + 1); out << " c r i t e r i o n W ; . c r i t e r i o n . d i s p l a y T r e e ( o u t , indent + 2); } ScopeSet *MuOptStmtMult i setRemove::deps(uint reqNum = 0 ) const •£ ScopeSet * r e s u l t , *temp; i f (reqNum == 0 ) reqNum = nextReqNumQ ; i f (depLoop(reqNum)) r e t u r n new ScopeSet; r e s u l t = . index .deps (reqNum); temp = _target->deps(reqNum); r e s u l t - > i n s e r t ( t e m p - > b e g i n ( ) , temp->end()); d e l e t e temp; temp = . c r i t e r i o n . d e p s ( r e q N u m ) ; r e s u l t - > i n s e r t ( t e m p - > b e g i n ( ) , temp->end()); d e l e t e temp; r e t u r n r e s u l t ; } 110 MuOptStmtNull::MuOptStmtNull() : MuOptStmt(Null) { t i fdef MUOPT.DEBUG cerr << "MuOptStmtNull::MuOptStmtNull()\n"; tendif } MuOptStmtNull::"MuOptStmtNull() { } void MuOptStmtNull::displayTree(ostreamfe out, uint indent) const •( t i fdef MUOPT.DEBUG cerr << "MuOptStmtNull::displayTree(int) const\n"; tendif indentLine(out, indent); out << "null statement\n"; } ScopeSet *MuOptStmtNull::deps(uint reqNum = 0) const { return new ScopeSet; } A.2.9 mu_opt_typedecl.cc / / mu_opt_decl.cc - * - C++ - * -tinclude "mu_opt_decl.h" tinclude "mu_opt_param.h" tinclude "mu.opt.typedecl.h" map<typedecl*,MuOptTypeDecl*> MuOptTypeDecl::_existing; MuOptTypeDecl::"MuOptTypeDecl() { } void MuOptTypeDecl::displayTree(ostreamft out, uint indent) const { t i fdef MUOPT.DEBUG cerr << "MuOptTypeDecl::displayTree(int) const\n"; tendif indentLine(out, indent); out << "decl.class is Type \"" « nameO << "\"\n"; } MuOptTypeDecl *MuOptTypeDecl::newMuOptTypeDecl(typedecl *td) { MuOptTypeDecl *result = NULL; i f(td) i f ( .existing.find(td) == .exist ing.endO) { switch(td->gettypeclass()) { case typedecl::Enum: result = new MuOptTypeDeclEnum(dynamic_cast<enumtypedecl*>(td)); break; case typedecl::Range: result=new MuOptTypeDeclRange(dynamic_cast<subrangetypedecl*>(td)); break; case typedecl::Array: result = new MuOptTypeDeclArray(dynamic_cast<arraytypedecl*>(td)); break; 111 case typedecl::MultiSet: result = new MuOptTypeDeclMultiSet(dynamic_cast<multisettypedecl*> (td)); break; case typedecl::MultiSetID: result = new MuOptTypeDeclMultiSetID(dynamic_cast<multisetidtypedecl*>(td)); break; case typedecl::Record: result=new MuOptTypeDeclRecord(dynamic_cast<recordtypedecl*>(td)); break; case typedecl::Scalarset: result = new MuOptTypeDeclScalarset(dynamic_cast<scalarsettypedecl*>(td)); break; case typedecl::Union: result = new MuOptTypeDeclUnion(dynamic_cast<uniontypedecl*>(td)); break; case typedecl::Error_type: result = new MuOptTypeDeclError(dynamic_cast<errortypedecl*>(td)); break; default: assert(O); break; > _existing[td] = result; }else { result = _existing[td]; #ifdef MUOPT.DEBUG cerr « "reissuing existing typedecl\n"; #endif } return result; } MuOptTypeDeclEnum::MuOptTypeDeclEnum(enumtypedecl *n) : MuOptTypeDecKEnum, n ? n->name : NULL), _node(n), _left(n ? n->getleft() : -1), _right(n ? n->getright() : -1), _idvalues(n ? n->getidvalues() : NULL) { tfifdef MUOPT.DEBUG cerr « "MuOptTypeDeclEnum::MuOptTypeDeclEnum(enumtypedecl*)\n"; #endif > MuOptTypeDeclEnum:: "MuOptTypeDeclEnumO { } void MuOptTypeDeclEnum::displayTree(ostream. out, uint indent) const { Sifdef MUOPT.DEBUG cerr « "MuOptTypeDeclEnum::displayTree(int) const\n"; #endif MuOptTypeDecl::displayTree(out, indent); indentLine(out, indent + 1); out « "typeclass is Enum\n"; indentLine(out, indent + 2); out << "left " << . l e f t « ", right " « .r ight « "\n"; indentLine(out, indent + 2); out << "idvalues\n"; .idvalues.displayTree(out, indent + 3); 112 } ScopeSet *MuOptTypeDeclEnum: : deps (uint reqNum = 0) const { if(reqNum == 0) reqNum = nextReqNumQ ; if(depLoop(reqNum)) return new ScopeSet; return _idvalues.deps(reqNum); > MuOptTypeDeclRange::MuOptTypeDeclRange(subrangetypedecl *n) : MuOptTypeDecl(Range, n ? n->name : NULL), _node(n), _left(n ? n->getleft() : -1 ) , _right(n ? n->getright() : -1) { #ifdef MUOPT.DEBUG cerr << "MuOptTypeDeclRange::MuOptTypeDeclRange(subrangetypedecl*)\n"; #endif > MuOptTypeDeclRange::"MuOptTypeDeclRange() { } void MuOptTypeDeclRange::displayTree(ostreamSt out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptTypeDeclRange::displayTree(int) const\n"; #endif MuOptTypeDecl::displayTree(out, indent); indentLine(out, indent + 1); out << "typeclass is Range\n"; indentLine(out, indent + 2); out << "left " « . l e f t « ", right " « .r ight « "\n"; } ScopeSet *MuOptTypeDeclRange::deps(uint reqNum = 0) const { return new ScopeSet; } MuOptTypeDeclArray::MuOptTypeDeclArray(arraytypedecl *n) : MuOptTypeDecKArray, n ? n->name : NULL), _node(n), .indexType(NULL), .elementType(NULL) { Sifdef MUOPT.DEBUG cerr << "MuOptTypeDeclArray::MuOptTypeDeclArray(arraytypedecl*)\n"; #endif if(n) { if(n->getindextype()) .indexType = MuOptTypeDecl::newMuOptTypeDecl(n->getindextype()); if(n->getelementtype()) .elementType = MuOptTypeDecl::newMuOptTypeDecl(n->getelementtype()); } } MuOptTypeDeclArray::"MuOptTypeDeclArrayQ { / /delete .indexType; //delete .elementType; } void MuOptTypeDeclArray::displayTree(ostreamfe out, uint indent) const { 113 t i fdef MUOPT.DEBUG cerr << "MuOptTypeDeclArray: :displayTree(int) const\n" ; tendif MuOptTypeDecl::displayTree(out, indent); indentLine(out, indent + 1); out << "typeclass is Array\n"; if(.indexType) { indentLine(out, indent + 1); out << "[index type]\n"; _indexType->displayTree(out, indent + 2); } if(.elementType) { indentLine(out, indent + 1); out << "[element type]\n"; _elementType->displayTree(out, indent + 2); } } ScopeSet *MuOptTypeDeclArray::deps(uint reqNum = 0) const { ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; if(.indexType) result = _indexType->deps(reqNum) ; else result = new ScopeSet; if(.elementType) { temp = _elementType->deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; } return result; } MuOptTypeDeclMultiSet::MuOptTypeDeclMultiSet(multisettypedecl *n) : MuOptTypeDecl(Multiset, n ? n->name : NULL), _node(n) { t i fdef MUOPT.DEBUG cerr << "MuOptTypeDeclMultiSet::MuOptTypeDeclMultiSet(multisettypedecl*)\n"; tendif / /assert(O); } MuOptTypeDeclMultiSet: : "MuOptTypeDeclMultiSetO { } void MuOptTypeDeclMultiSet::displayTree(ostreamfe out, uint indent) const { t i fdef MUOPT.DEBUG cerr « "MuOptTypeDeclMultiSet::displayTree(int) const\n"; tendif MuOptTypeDecl::displayTree(out, indent); indentLine(out, indent + 1); 114 out << "typeclass is MultiSet\n"; } ScopeSet *MuOptTypeDeclMultiSet: :deps (uint reqNum = 0) const { / /assert(O); return new ScopeSet; / * ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; result = .deps(reqNum); temp = .deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; return result; * / } MuOptTypeDeclMultiSetID::MuOptTypeDeclMultiSetID(multisetidtypedecl *n) : MuOptTypeDecl(MultiSetID, n ? n->name : NULL), _node(n) { #ifdef MUOPT.DEBUG cerr « "MuOptTypeDeclMultiSetID::" "MuOptTypeDeclMultiSetID(multisetidtypedecl*)\n"; #endif assert(0); > MuOptTypeDeclMultiSetID:: "MuOptTypeDeclMultiSetlDO { } void MuOptTypeDeclMultiSetID::displayTree(ostreamfe out, uint indent) const{ #ifdef MUOPT.DEBUG cerr « "MuOptTypeDeclSetID::displayTree(int) const\n"; ftendif MuOptTypeDecl::displayTree(out, indent); indentLine(out, indent + 1); out << "typeclass is MultiSetID\n"; } ScopeSet *MuOptTypeDeclMultiSetID::deps(uint reqNum = 0) const { assert(O); return NULL; / * ScopeSet *result, *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; result = .deps(reqNum); 115 temp = .deps(reqNum); resuit->insert(temp->begin(), temp->end()); delete temp; return result; } MuOptTypeDeclRecord::MuOptTypeDeclRecord(recordtypedecl *n) : MuOptTypeDecl(Record, n ? n->name : NULL), _node(n), _fields(n ? n->getfieldsO : NULL) { t i fdef MUOPT.DEBUG cerr << "MuOptTypeDeclRecord::MuOptTypeDeclRecord(recordtypedecl*)\n"; tendif } MuOptTypeDeclRecord::"MuOptTypeDeclRecordO { } void MuOptTypeDeclRecord::displayTree(ostreamfe out, uint indent) const { (tifdef MUOPT.DEBUG cerr << "MuOptTypeDeclRecord::displayTree(int) const\n"; (tendif MuOptTypeDecl::displayTree(out, indent); indentLine(out, indent + 1); out << "typeclass is RecordXn"; indentLine(out, indent + 2); out « "fields\n"; . f ields.displayTree(out, indent + 3); } ScopeSet *MuOptTypeDeclRecord::deps(uint reqNum = 0) const { if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; return _f ields.deps(reqNum); } MuOptTypeDeclScalarset::MuOptTypeDeclScalarset(scalarsettypedecl *n) : MuOptTypeDecl(Scalarset, n ? n->name : NULL), _node(n), _left(n ? n->getleft() : -1), _right(n ? n->getright() : -1), . idvalues(n ? n->getidvalues() : NULL) { (tifdef MUOPT.DEBUG cerr << "MuOptTypeDeclScalarset::MuOptTypeDeclScalarset(scalarsettypedecl*)\n"; tendif //assert(!n->useless); } MuOptTypeDeclScalarset::"MuOptTypeDeclScalarset() { } void MuOptTypeDeclScalarset::displayTree(ostream_ out, uint indent) const { t i fdef MUOPT.DEBUG 116 cerr << "MuOptTypeDeclScalarset::displayTree(int) const\n"; tendif MuOptTypeDecl::displayTree(out, indent); indentLine(out, indent + 1); out << "typeclass is Scalarset\n"; indentLine(out, indent + 2); out << "further dependencies ignored\n"; } ScopeSet *MuOptTypeDeclScalarset:: deps (uint reqNum = 0) const •( ScopeSet *resu l t ; / / , *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) return new ScopeSet; result = .idvalues.deps(reqNum); /* temp = .deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; */ return result; } MuOptTypeDeclUnion::MuOptTypeDeclUnion(uniontypedecl *n) : MuOptTypeDecl(Union, n ? n->name : NULL), _node(n), _unionmembers(n ? n->getunionmembers() : NULL) { (tifdef MUOPT.DEBUG cerr << "MuOptTypeDeclUnion::MuOptTypeDeclUnion(uniontypedecl*)\n"; (tendif } MuOptTypeDeclUnion::"MuOptTypeDeclUnionO { } void MuOptTypeDeclUnion::displayTree(ostreamft out, uint indent) const { t i fdef MUOPT.DEBUG cerr << "MuOptTypeDeclUnion::displayTree(int) const\n"; tendif MuOptTypeDecl::displayTree(out, indent); indentLine(out, indent + 1); out << "typeclass is UnionNn"; indentLine(out, indent + 2 ) ; out << "further dependencies ignored\n"; } ScopeSet *MuOptTypeDeclUnion:: deps (uint reqNum = 0) const •( ScopeSet *resu l t ; / / , *temp; if(reqNum == 0) reqNum = nextReqNumO; if(depLoop(reqNum)) 117 return new ScopeSet; result = _unionmembers.deps(reqNum); / * temp = .deps(reqNum); result->insert(temp->begin(), temp->end()); delete temp; */ return result; MuOptTypeDeclError: :MuOptTypeDeclError(errortypedecl *n) : MuOptTypeDecl(Error, n ? n->name : NULL), _node(n) { t i fdef MUOPT.DEBUG cerr << "MuOptTypeDeclError::MuOptTypeDeclError(errortypedecl*)\n"; #endif } MuOptTypeDeclError::"MuOptTypeDeclError() { } void MuOptTypeDeclError::displayTree(ostream_ out, uint indent) const { #ifdef MUOPT.DEBUG cerr << "MuOptTypeDeclError::displayTree(int) const\n"; #endif MuOptTypeDecl::displayTree(out, indent); indentLine(out, indent + 1); out « "Error.typeNn"; } ScopeSet *MuOptTypeDeclError::deps(uint reqNum = 0) const { return new ScopeSet; } A . 3 O t h e r F i les A.3.1 Murphi3.1-muopt.patch dif f -ur Murphi.orig/include/mu.verifier.h Murphi3.l/include/mu_verifier.h Murphi.orig/include/mu.verifier.h Thu Jan 28 23:49:11 1999 +++ Murphi3.1/include/mu_verifier.h Mon Aug 2 13:05:26 1999 aa - 9 5 , 7 +95,6 ae #define BITS(type) ((int)sizeof (type) * CHAR.BIT) Sendif -typedef char bool; typedef void (*proc) (void); typedef bool (*boolfunc) (void); d i f f -ur Murphi.orig/src/Makefile Murphi3.1/src/Makefile — Murphi.orig/src/Makefile Thu Jan 28 23:49:11 1999 +++ Murphi3.1/src/Makefile Thu Aug 19 13:00:03 1999 aa -38,20 +38,23 aa 118 (tCPLUSPLUS = xlC -+ -Q! # choice of the options -CFLAGS = -04 +CFLAGS = -g -04 - I . - I . . / . . /muopt SCFLAGS = -04 -pipe -s tat ic # SCFLAGS = -stat ic # #CFLAGS = -w # SCFLAGS = -w -03 S +LDFLAGS = -L . . / . . /muopt +LIBS = -lmuopt + OBJS = \ cpp_code.o \ cpp_code_as.o \ lex.yy.o \ y.tab.o \ cpp_sym.o \ cpp_sym_aux.o \ cpp_sym_decl.o \ + cpp_sym.o \ + cpp_sym_aux.o \ + cpp_sym_decl.o \ decl.o \ error.o \ expr.o \ ee -65,8 +68,8 aa ######################################## # Makefile grammar -mu: $(0BJS) $(CPLUSPLUS) -o mu $(CFLAGS) $(0BJS) +mu: $(0BJS) . . / . . /muopt/l ibmuopt.a + $(CPLUSPLUS) -o mu $(CFLAGS) $(0BJS) $(LDFLAGS) $(LIBS) mu. o: mu. C mu. h $(CPLUSPLUS) -c $(CFLAGS) mu.C di f f -ur Murphi. orig/src/expr .h Murphi3.1/src/expr.h Murphi.orig/src/expr.h F r i Jan 29 00:28:10 1999 +++ Murphi3.1/src/expr.h Wed Sep 15 17:53:52 1999 aa -323,6 +323,9 aa ********************/ class designator: public expr { + friend MuOptDesignator; + friend MuOptDesignatorlnstance; + friend MuOptDesignatorList; / / variables designator * le f t ; ste * origin; / * an ident i f ier; * / d i f f -ur Murphi.orig/src/mu.C Murphi3.1/src/mu.C Murphi.orig/src/mu.C F r i Jan 29 00:28:10 1999 +++ Murphi3.1/src/mu.C Thu Aug 5 13:56:01 1999 aa -63,6 +63,7 aa */ ((include "mu.h" +#include <mu_opt.h> ((include <string.h> # options for g++ # options for g++ # options for OCC # options for DCC 119 tinclude <new.h> aa -442,6 +443,8 aa error = yyparseQ; i f ( ! error kk Error .getnumerrorsO == 0 ) { + MuOptRoot muo(theprog); + muo.optimize(); codefile = setup_outfile( args->filename ); theprog->generate_code(); fclose(codefile); d i f f -ur Murphi.orig/src/mu.h Murphi3.1/src/mu.h Murphi.orig/src/mu.h F r i Jan 29 13:56:53 1999 +++ Murphi3.1 /src /mu.h Wed Sep 15 17:54:14 1999 aa -110,7 +110,6 aa boolean constants * * * * * * * * * * * * * * * * * * * * / -typedef char bool; / * just for my sake. * / tdefine TRUE 1 tdefine FALSE 0 aa -388,6 +387,7 88 •C s te l i s t * f i r s t ; s te l i s t *last; + friend class MuOptSTEChain; public: s teco lKste *s) { f i r s t = last = new ste l i s t (s, NULL); } aa -469,7 +471,7 aa char * bodyname, bool unfair) : rulename(rulename), conditionname(conditionname), bodyname(bodyname), next(NULL), unfair(unfair) {}; + unfair (unfair) , next(NULL) O ; int print_rules(); / * print out a l i s t of rulerecs. * / } ; aa - 4 9 i , 8 +493,9 aa char * rightconditionname, l ive.type livetype) : rulename(rulename), preconditionname(preconditionname), l ivetype(livetype), leftconditionname(leftconditionname), rightconditionname(rightconditionname), next(NULL) {}; + leftconditionname(leftconditionname), + rightconditionname(rightconditionname), + livetype(livetype) , next(NULL) O ; int print_l iverules( ) ; }; dif f -ur Murphi .orig/src/rule .C M u r p h i 3 . 1 / s r c / r u l e . C Murphi .orig/src/rule .C Mon Mar 22 22:17:50 1999 +++ M u r p h i 3 . 1 / s r c / r u l e . C Thu Sep 16 14:51:03 1999 aa -96 ,7 +96,24 aa / / mentioned in the condition go f i r s t rearrange_enclosures(); + copy_enclosures(); } 120 +void simplerule::copy_enclosures() { + ste *in = enclosures, *last = NULL; + enclosures = NULL; + while(in) { + ste *copy = new ste(*in); + copy->next = NULL; + i f ( la s t ) + last->next = copy; + else + enclosures = copy; + last = copy; + in = in->next; + } +} simplerule * simplerule::SimpleRuleList = NULL; d i f f -ur Murphi .orig/src/rule .h Murphi3.1/src/rule.h Murphi .orig/src/rule .h F r i Jan 29 00:28:10 1999 +++ Murphi3.1/src/rule.h Thu Sep 16 14:51:23 1999 aa -138,9 +138,10 aa / / code generation v ir tua l char *generate_code(); CountSize(ste * enclosures); + int CountSize(ste * enclosures); void rearrange_enclosures(); + void copy_enclosures(); int gets izeQ { return size; } }; A. 3.2 Makefile CXX = g++ CXXFLAGS = -Wall - I . -I . . /Murphi3.1/src - I . . / s r c -g LD = g++ -shared - fpic LDFLAGS = LIBS = RANLIB = ranl ib OFILES = mu_opt_base.o mu_opt_decl.o mu_opt_expr.o mu_opt_param.o \ mu_opt_root.o mu_opt_rule.o mu_opt_ste.o mu_opt_stmt.o \ mu_opt.typedecl.o TARGET = libmuopt.a a l l : $(TARGET) i n s t a l l tests: a l l libmuopt.a: $(OFILES) rm - f $3 ar cr $3 $~ $(RANLIB) $8 121 libmuopt.so: $(0FILES) rm - f $® $(LD) $" $(LDFLAGS) $(LIBS) -o $S testprog: testprog.o $(CXX) $" $(LDFLAGS) -lmuopt $(LIBS) -o $ 3 mu_opt_base.o: mu_opt_base.cc mu_opt_base.h mu_opt_decl.o: mu_opt_decl.cc mu_opt_decl.h mu_opt_param.h \ mu_opt_typedecl.h mu_opt_expr.o: mu_opt_expr.cc mu_opt_expr.h mu_opt_base.h mu_opt_param.o: mu_opt_param.cc mu_opt_param.h mu_opt_root.o: mu_opt_root.cc mu_opt_root.h mu_opt_rule.o: mu_opt_rule.cc mu_opt_rule.h mu_opt_ste.o: mu_opt_ste.cc mu_opt_ste.h mu_opt_decl.h mu_opt_stmt.o: mu_opt_stmt.cc mu_opt_stmt.h mu_opt_typedecl.o: mu_opt_typedecl.cc mu_opt_typedecl.h touch $a mu_opt.h: mu_opt_base.h mu_opt_decl.h mu_opt_expr.h mu_opt_root.h \ mu_opt_rule.h mu_opt_ste.h mu_opt_stmt.h mu_opt_decl.h: mu_opt_base.h mu_opt_ste.h mu_opt_stmt.h mu_opt_expr.h: mu_opt_base.h mu_opt_ste.h mu_opt_param.h: mu_opt_decl.h mu_opt_root.h: mu_opt_base.h mu_opt_ste.h mu_opt_rule.h mu_opt_rule.h: mu_opt_base.h mu_opt_ste.h mu_opt_expr.h mu_opt_stmt.h mu_opt_ste.h: mu_opt_base.h mu_opt_stmt.h: mu_opt_base.h mu_opt_expr.h mu_opt_typedecl.h: mu_opt_decl.h i n s t a l l : $(TARGET) # cp $(TARGET) ${exec_prefix}/lib # cp $(TARGET) . . / l i b clean: rm - f *" *.o a.out core veryclean: clean rm - f libmuopt.a libmuopt.so testprog 122 Appendix B Firewire Model Source B . l Novice Firewire Model This partial model of IEEE 1394 [13] is the one tested in Chapter 5. It was written Fall 1998, by the author, at the beginning of his graduate studies. At that time the author was a Mur</? novice. The model is a part of the cable physical layer [12], specifically the bus reset and tree identification state machines. — 1394.m — $Id: 1394.m,v 1.10 1998/11/25 17:32:54 bwinters Exp $ — Brian Winters — Revision history: 11/24/98 Worked out startup problems. Able to reach a l l states up to SO ( a l l I've implemented so far ) . Statespace blows up doing f u l l evaluation of that statespace though. 11/22/98 Have the standard. Implementing PHY from their code. 11/10/98 Started using CVS (I'm sleeping better already). Implementing cables between nodes as a resolution function of the outputs of those two nodes. 11/03/98 I n i t i a l version. Linear arrangement of N nodes. const N: 2; — number of nodes HIGHPORT: 1; — highest numbered port possible per node —HIGHFIFO.DEPTH: 0; — highest numbered entry in a FIFO 123 TIMER_MAX: 4; — table 4-32 CONFIG.TIMEOUT: 3; — 5; — 14; — defined as 16384 FORCE_ROOT_TIMEOUT: 2; — 4; — 13; — defined as >=8192 and <= CONFIG.TIMEOUT ROOT.CONTEND.FAST: i ; — l ; — 2; --- defined iS 24 ROOT_CONTEND_SLOW: 2; — 2; — 3; --- defined as 56 RESET.TIME: 3; — 5; — 14; — defined as 16384 RESET.WAIT: 4; — 6; — 15; — defined as 16400 MAX_ARB_STATE_TIME: RESET .WAIT; — semi-contrived, see table 4-44 GAP_COUNT_MAX: 2; — 3; — 4; — defined as 63 type IDnum: 0..(N-1); Portnum: 0..HIGHPORT; — FIFOnum: 0..HIGHFIFO.DEPTH; irange: 0..(HIGHPORT+1); PHY.state: enum { RO, R l , TO, T l , T2, T3, SO, S l , S2, S3, S4, AO, A l , A2, A3, A4, A5, A6 }; — bogus types dataBit: boolean; baserate.time: 0..TIMER.MAX; timer: baserate.time; gap.counter: 0..GAP_COUNT_MAX; — 4.4 Cable PHY operation, table 4-37 phyData: enum { L , H, Z }; speedCode: enum { S100, S200, S400 }; portData : record TPA: phyData; TPB: phyData; end; — 4.3.3: transmitted l ine states, table 4-27 ArbLineStateTX: enum { TX.IDLE, TX.REQUEST, TX.GRANT, TX.PARENT.NOTIFY, TX.DATA.PREFIX, TX.CHILD.NOTIFY, TX.IDENT.DONE, TX.DATA.END, TX.BUS.RESET }; — 4.3.3: received l ine states, table 4-28 ArbLineStateRX: enum { RX.IDLE, RX.PARENT.NOTIFY, RX.REQUEST.CANCEL, RX.IDENT.DONE, RX_SELF.ID_GRANT, RX.REQUEST, RX.ROOT.CONTENTION, RX.GRANT, RX_PARENT_HANDSHAKE, RX_DATA_END, RX.CHILD.HANDSHAKE, RX_DATA_PREFIX, RX.BUS.RESET }; — PORT definit ion port: 124 record 4.3.9 Port variables chi ld: boolean; connected: boolean; child_ID_complete: boolean; max_peer_speed: MaxSpeed; —NYM speed_0K: boolean; —NYM data: portData; — this one not exp l i c i t ly defined, guessing here end; NODE definit ion node: record 4.3.7 Cable PHY node constants NPORT: irange; PHY.DELAY.CATEGORY: 0( . .3); — this can only be 0 in current spec PHY.SPEED: MaxSpeed; — NYM POWER_CLASS: 0..7; — don't care about physical power characteristics CONTENDER: boolean; 4.3.8 Node variables, table 4-35 arb_enable: boolean; cable_power_active: boolean; force_root: boolean; gap_count: gap_counter; — guessing on variable type here initiated_reset: boolean; l ink_active: boolean; more_packets: boolean; parent_port: Portnum; physical_ID: IDnum; receive.port: Portnum; root: boolean; 4.4 Cable PHY operation, table 4-37, implied internal variables f ifo_rd_ptr: FIFOnum; fifo_wr_ptr: FIFOnum; FIFO_DEPTH: FIFOnum; FIFO: array[FIFOnum] of dataBit; waiting.for_data_start: boolean; rx_speed: speedCode; arb_timer: timer; root_test: boolean; contend_time: baserate.time; child_count: irange; lowest_unidentified_child: Portnum; al l_child_ports_identif ied: boolean; self_ID_complete: boolean; requesting_child: Portnum; force_root: boolean; — see above end.of.reception: boolean; link_req_active: boolean; arb_enable: boolean; — see above old_connect: array[Portnum] of boolean; — actually array of NPORT bus_init ial ize_active: boolean; gap_count.reset.disable: boolean; 125 — variables to emulate the physical aspects of a node ports: array[Portnum] of port; — current state of the node Pstate: PHY_state; end; var nodes: array[IDnum] of node; — FUNCTIONS — mapping functions, to model the physical wiring — assumes N=2 function trans_good(n: IDnum; port_number: Portnum): boolean; begin return ((n=0 k port_number=l) I (n=l k port_number=0)); end; — assumes N=3 —function trans_good(n: IDnum; port_number: Portnum): boolean; —begin — assert (N=3 & HIGHP0RT=1) "N and/or HIGHPORT do not match"; return ((n=0 k port_number=l) I (n=l) I (n=2 k port_number=0)); —end; — assumes N=2 function trans_node(n: IDnum; port_number: Portnum): IDnum; begin if(n=0 k port_number=l) then return 1; elsif(n=l It port_number=0) then return 0; end; end; ~ assumes N=3, HIGHP0RT=1 —function trans_node(n: IDnum; port.number: Portnum): IDnum; —begin — assert (N=3 k HIGHP0RT=1) "N and/or HIGHPORT do not match"; if(n=0 k port_number=l) then return 1; elsif(n=l k port_number=0) then return 0; elsif(n=l & port_number=l) then return 2; elsif(n=2 & port_number=0) then return 1; else error "Invalid node/port combination"; end; —end; — assumes N=2 function trans_port(n: IDnum; port.number: Portnum): Portnum; 126 begin if(n=0 & port_number=l) then return 0; elsif(n=l & port.number=0) then return 1; end; end; — assumes N=3, HIGHP0RT=1 --function trans_port(n: IDnum; port.number: Portnum): Portnum; —begin — assert (N=3 k HIGHP0RT=1) "N and/or HIGHPORT do not match"; if(n=0 k port_number=l) then return 0; elsif(n=l k port.number=0) then return 1; elsif(n=l k port_number=l) then return 0; elsif(n=2 fe port_number=0) then return 1; else error "Invalid node/port combination"; end; —end; — hardware functions, prototyped from table 4-37 —function random.boolO : boolean; —begin pseudorandom - w i l l protocol work even with bad randomizer? return true; return false; return random.value; —end; —procedure portT(n: IDnum; port.number: Portnum; txData: portData); procedure portT(n: IDnum; port.number: Portnum; txData: ArbLineStateTX); begin al ias p: nodes[n].ports[port.number].data do — from table 4-27 switch txData case TX. .IDLE: p.TPA := Z; p.TPB := Z; case TX. .REQUEST: p.TPA := Z; p.TPB := L; case TX. .GRANT: p.TPA := Z; p.TPB := L; case TX. .PARENT.NOTIFY p.TPA := L; p.TPB := Z; case TX. .DATA.PREFIX: p.TPA := L; p.TPB := H; case TX. .CHILD.NOTIFY: p.TPA := H; 127 p.TPB := Z; case TX_IDENT_DONE: p.TPA := H; p.TPB := Z; case TX.DATA.END: p.TPA := H; p.TPB := L; case TX_BUS_RESET: p.TPA := H; p.TPB := H; end; end; end; function resolve(a, b: phyData): phyData; begin if(a=Z) then return b; end; if(b=Z I a=b) then return a; end; return Z; end; —function portR(n, port_number: IDnum): portData; function portR(n, port.number: IDnum): ArbLineStateRX; var Tn, Tp: IDnum; otherA, otherB: phyData; begin otherA := Z; otherB := Z; if(trans_good(n, port.number)) then Tn := trans_node(n, port.number); Tp := trans_port(n, port.number); otherA := nodes[Tn].ports[Tp].data.TPA; otherB := nodes[Tn].ports[Tp].data.TPB; end; al ias pt: nodes[n].ports[port.number].data do — from table 4-28 if(resolve(pt.TPA, otherB) return RX.IDLE; elsif(resolve(pt.TPA, otherB) return RX.PARENT.NOTIFY; — elsif(resolve(pt.TPA, otherB) return RX.IDENT.DONE; elsif(resolve(pt.TPA, otherB) return RX.SELF.ID.GRANT; — elsif(resolve(pt.TPA, otherB) return RX.ROOT.CONTENTION; elsif(resolve(pt.TPA, otherB) return RX.PARENT.HANDSHAKE; elsif(resolve(pt.TPA, otherB) return RX.CHILD.HANDSHAKE; elsif(resolve(pt.TPA, otherB) return RX.DATA.PREFIX; elsif(resolve(pt.TPA, otherB) return RX.BUS.RESET; end; end; end; Z & resolve(pt.TPB, otherA) = Z) then = Z k resolve(pt.TPB, also RX.REQUEST.CANCEL = Z k resolve(pt.TPB, = L k resolve(pt.TPB, also RX.REQUEST = L fe resolve(pt.TPB, - also RX.GRANT = L & resolve(pt.TPB, — also RX.DATA.END = H & resolve(pt.TPB, = H k resolve(pt.TPB, = H & resolve(pt.TPB, otherA) = L) then otherA) = H) then otherA) = Z) then otherA) = L) then otherA) = H) then otherA) = Z) then otherA) = L) then otherA) - H) then function portRcomp(n, port.number: IDnum; c: ArbLineStateRX): boolean; var r: ArbLineStateRX; begin 128 r := portR(n, port.number); switch r case RX_PARENT_NOTIFY: i f (c = RX_REQUEST_CANCEL) then return true; end; case RX_SELF_ID_GRANT: i f (c = RX.REQUEST) then return true; end; case RX_R00T_C0NTENTI0N: i f (c = RX.GRANT) then return true; end; case RX_PARENT_HANDSHAKE: i f (c = RX.DATA.END) then return true; end; end; return (r = c); end; —procedure portTspeed(n, port_number: IDnum; speed: speedCode); —function portRspeed(n, port_number: IDnum): speedCode; — 4.4.2.1.2 Bus reset actions and conditions function bus_reset_signal_received(n: IDnum): boolean; — table 4-44 var i : irange; begin i:=0; while(i < nodes[n].NPORT) do if(nodes[n].ports[i] .connected & portRcomp(n, i , RX.BUS.RESET)) then return true; end; i:=i+l; end; return false; end; function connection_state_change(n: IDnum): boolean; — table 4-44" var state_change: boolean; i : irange; begin state_change := false; i:=0; while(i < nodes[n].NPORT) do if(nodes[n].ports[i].connected != nodes[n].old.connect[i] ) then state_change := true; nodes[n].old.connect[i] := !nodes[n].old.connect[i]; end; i:=i+l; end; return state.change; end; procedure reset_start_actions(n: IDnum); — table 4-44 var i : irange; 129 begin nodes[n].root := false; nodes[n].physical_ID := 0; nodes[n].child_count := 0; nodes[n].bus_initialize_active := true; if(nodes[n].gap_count_reset_disable) then nodes[n].gap_count_reset_disable := false; else nodes[n].gap.count := GAP_C0UNT_MAX; —hard coded to 0x3F in table 4-44 end; i:=0; while(i < nodes[n].NPORT) do if(nodes[n].ports[i].connected) then portT(n, i , TX.BUS.RESET); else portT(n, i , TX.IDLE); end; nodes[n].ports[i] .child := false; nodes[n].ports[i].child.ID.complete := false; i:=i+l; end; nodes[n].arb_timer := 0; end; procedure reset_wait_actions(n: IDnum); — table 4-44 var i : irange; begin i:=0; vh i l e ( i < nodes[n].NPORT) do portT(n, i , TX.IDLE); i:=i+l; end; nodes[n].arb.timer := 0; end; function reset_complete(n: IDnum): boolean; — table 4-44 var i : irange; begin i:=0; while(i < nodes[n].NPORT) do if(!portRcomp(n, i , RX_IDLE) & !portRcomp(n, i , RX.PARENT.NOTIFY) _ nodes[n].ports[i].connected) then return false; end; i:=i+l; end; return true; end; function arb_state_timeout(n: IDnum): boolean; — support for figure 4-22 begin alias nd: nodes[n] do al ias st: nd.Pstate do return ((st != Rl) 6 (st != AO) & (st != A5) & (st != A6) ft. (nd.arb.timer >= MAX.ARB_STATE.TIME)); end; end; end; — 4.4.2.2.2 Tree-ID actions and conditions 130 procedure tree_ID_start_actions_interp_l(n: IDnum); — table 4-45 var i , temp_count: irange; begin nodes[n].arb.timer := 0; — LOOP FOREVER??? EXCUSE ME???? — my suspicion here is that they intend that this be going on as some — sort of background process that is always updating child count, but — on second thought that doesn't make sense, because we immediately go — into a reset state i f our connections change while(true) do temp.count := 0; i:=0; while(i<nodes[n].NPORT) do — formatting of standard is ambiguous here; using C code and not indention - - my suspicion is that this interpretation is WRONG, but we' l l see if(!nodes[n].ports[i].connected I portRcomp(n, i , RX.PARENT.NOTIFY)) then nodes[n].ports[i] .child := true; temp.count := temp.count + 1; nodes [n].child.count := temp.count; end; i:=i+l; end; end; end; procedure tree_ID_start_actions_interp_2(n; IDnum); — table 4-45 var i , temp.count: irange; begin nodes[n].arb.timer := 0; temp.count := 0; i:=0; while(i<nodes[n].NPORT) do — formatting of standard is ambiguous here; using indention and not C code if(!nodes[n].ports[i].connected I portRcomp(n, i , RX.PARENT.NOTIFY)) then nodes[n].ports[i] .child := true; temp.count := temp.count + 1; end; i:=i+l; end; nodes[n].child.count := temp.count; end; end; procedure tree_ID_start_actions(n: IDnum); — table 4-45 begin tree . ID.s tart .act ions . interp. l (n) ; tree_ID_start_actions_interp_2(n); end; procedure child.handshake.actions(n: IDnum); — table 4-45 var i : irange; begin nodes [n].root := true; i:=0; while(i < nodes[n].NPORT) do if(nodes [n].ports[i].connected) then 131 i f(nodes[n].ports[i] .child) then portT(n, i , TX_CHILD_NOTIFY); else portT(n, i , TX_PARENT_NOTIFY); nodes[n].parent_port : = i ; nodes[n].root := false; end; end; i:=i+l; end; end; function child_handshake_complete(n: IDnum): boolean; — table 4-45 var i : irange; begin i : =0; while(i < nodes[n].NPORT) do if(nodes[n] .ports[ i ] .chi ld & nodes[n].ports[i].connected & !portRcomp(n, i , RX_CHILD_HANDSHAKE)) then return false; end; i:=i+l; end; return true; end; procedure root_contend_actions(n: IDnum; r: boolean); — table 4-45 var i : irange; begin i f (random.boolO) then i f ( r ) then nodes[n].contend.time := R00T_C0NTEND_SL0W; else nodes[n].contend_time := R00T_C0NTEND_FAST; end; i:=0; while(i < nodes[n].NPORT) do if(nodes[n].ports[i] .child) then portT(n, i , TX.CHILD.NOTIFY); else portT(n, i , TX.IDLE); end; i:=i+l; end; nodes[n].arb_timer := 0; end; procedure self_ID_start_actions(n: IDnum); — table 4-46 var i : irange; begin nodes[n].all_child_ports_identified := true; i:=0; while(i < nodes[n].NPORT) do if(nodes[n].ports[i].child_ID_complete) then portT(n, i , TX.DATA.PREFIX); else portT(n, i , TX.IDLE); i f (nodes[n] .ports[ i ] .chi ld _ nodes[n].ports[i].connected) then if(nodes[n].all_child_ports_identified) then 132 nodes[n].lowest_unidentified_child := i ; end; nodes[n].all_child_ports_identified := false; end; end; i:=i+l; end; end; procedure self.ID_grant_actions(n: IDnum); — table 4-46 var i : irange; begin i:=0; while (Knodes [n] .NPORT) do if(!nodes[n].all_child_ports_identified fe ( i = nodes[n].lowest_unidentified_child)) then portT(n, i , TX.GRANT); else portTCn, i , TX_DATA_PREFIX); end; i:=i+l; end; end; procedure self_ID_receive_actions(n; IDnum); — table 4-46 var i : irange; begin portT(n, nodes[n].receive_port, TX_IDLE); — receive.actions(n); nodes[n].physical_ID := nodes[n].physical.ID + 1; i:=0; while (Knodes [n] .NPORT) do portTCn, i , TX.IDLE); i:=i+l; end; end; —procedure self_ID_transmit_actions(n; IDnum); — table 4-46 —var last_SID_packet, SID_pkt.number, port.number: irange; --begin - - last_SID_packet := 1; — (nodes[n].NPORT + 4) / 8; nodes [n].self_ID_complete := false; nodes[n].receive_port := nodes[n].NPORT; — start_tx_packet(n,. S100); — SID_pkt_number := 0; while(SID_pkt_number <= last_SID_pkt) begin — abstracting away SID packet construction while(port.number < ((SID.pkt.number + 1)*8 - 5)) do — abstracting away more SID packet construction port.number:=port_number+l; end; — abstracting away even more SID packet construction if(SID.pkt.number = last.SID.pkt) then — don't send quadlets - - stop_tx_packet(n, TX.DATA.END, S100); else stop_tx_packet(n, TX.DATA.PREFIX, S100); end; SID.pkt.number:=SID_pkt_number+l; end; 133 port.number:=0; while(port.number < nodes[n].NPORT) do if(port.number == parent.port) then portT(n, port.number, TX.IDENT.DONE); — portTspeedO ; — wait.timeO ; — portTspeedO ; — PH.EVENT.ind(SELF_ID_COMPLETE, physical.ID, root); else portT(n, port.number, TX.IDLE); end; port.number:=port_number+l; — bad bug in standard I think end; self.ID.complete := true; —end; — RULESETS — random value hack ruleset r: boolean do — state machine by node ruleset n: IDnum do alias nd: nodes[n] do alias st: nd.Pstate do rule "increment timer (modeling hack)" nd.arb.timer < TIMER.MAX ==> begin nd.arb.timer := nd.arb.timer + 1; end; rule "Transition All:R0a (4.4.2.1.1)" bus_reset_signal_received(n) ==> begin st := R0; reset .start .actions(n); — 4.4.2.1 — PH.STATE.ind(BUS_RESET_START) (4.4.2.1) nd. init iated.reset := false; end; rule "Transition All:R0b (4.4.2.1.1)" ( PH_CONT.req(bus_reset) I connection.state.change(n) I arb_state_timeout(n)) ==> begin st := R0; — PH.STATE.ind(BUS_RESET_START) (4.4.2.1) nd. init iated.reset := true; end; rule "Transition R0:R1 (4.4.2.1.1)" ((st = R0) & (nd.arb.timer >= RESET.TIME)) ==> begin st := R l ; reset.wait.actions(n); — 4.4.2.1 end; rule "Transition R1:R0 (4.4.2.1.1)" ((st = Rl) & (nd.arb.timer >= RESET.WAIT)) ==> begin st := R0; 134 reset_start_actions(n); — 4.4.2.1 end; rule "Transition R1:T0 (4.4.2.1.1)" ((st = Rl) & reset_complete(n)) ==> begin st := TO; tree_ID_start_actions(n); — 4.4.2.2 end; rule "Transition T0:T0 (4.4.2.2.1)" ((st = TO) & ((nd.arb.timer >= CONFIG.TIMEOUT) & (nd.child_count < (nd.NPORT - 1)))) ==> begin st := TO; — signal PH.STATE.ind(CONFIG.TIMEOUT) (4.4.2.2) tree_ID_start_actions(n); — 4.4.2.2 end; rule "Transition T0:T1 (4.4.2.2.1)" ((st = TO) & ((nd.child_count = nd.NPORT) I (((nd.force_root & (nd.arb.timer >= FORCE.ROOT.TIMEOUT))I (Ind.force_root & (nd.arb.timer >= 0))) & (nd.child.count = (nd.NPORT - 1))))) ==> begin st := T l ; child_handshake_actions(n); — 4.4.2.2 end; rule "Transition T1:T2 (4.4.2.2.1)" ((st = Tl) & child_handshake_complete(n)) ==> begin st := T2; end; rule "Transition T2:S0 (4.4.2.2.1)" ((st = T2) & (nd.root I portRcomp(n, nd.parent_port, RX.PARENT.HANDSHAKE))) ==> begin st := SO; self_ID_start_actions(n); end; rule "Transition T2:T3 (4.4.2.2.1)" ((st = T2) fc portRcomp(n, nd.parent_port, RX_R00T_C0NTENTI0N)) ==> begin st := T3; root_contend_actions(n, r ) ; — 4.4.2.2 end; rule "Transition T3:T2 (4.4.2.2.1)" ((st = T3) fe (portRcomp(n, nd.parent_port, RX_IDLE) & (nd.arb.timer > nd.contend_time))) ==> begin st := T2; portT(n, nd.parent_port, TX.PARENT.NOTIFY); — 4.4.2.2 end; rule "Transition T3:T1 (4.4.2.2.1)" ((st = T3) & (portRcomp(n, nd.parent_port, RX.PARENT.NOTIFY) & (nd.arb.timer > nd.contend_time))) ==> begin st := T l ; — 4.4.2.2: "node is now root" nd.ports[nd.parent_port].child := true; end; end; 135 end; end; - - state machine by node end; — random value — INITIALIZATION CODE startstate begin for n: IDnum do alias nd: nodesCn] do — 4.3.7 Cable PHY node constants nd.NPORT := HIGHPORT + 1; nd.PHY_DELAY_CATEGORY := 0; — this can only be 0 in current spec nd.PHY_SPEED := S100; — NYM nd.POWER_CLASS := 0; - - don't care about phys power characteristics nd.CONTENDER := false; — don't want to model resource manager role — 4.3.8 Node variables, table 4-35 nd.arb_enable := false; nd.cable_power_active := true; nd.force_root := false; — not going to model this yet nd.gap_count := ; — not sure what variable type this should be nd.initiated_reset := false; — should add some rules to allow a — node to choose to in i t ia te reset at — any time nd link_active = false; nd more_packets := false nd parent_port = 0; nd physical.ID = 0; nd receive_port := 0; nd root := fals i 4.4 Cable PHY operation, table 4-37, implied internal variables nd.fifo_rd_ptr := 0; nd.fifo_wr_ptr := 0; nd.FIFO.DEPTH := HIGHFIFO.DEPTH; for i : FIFOnum do nd.FIF0[i] := false; — just makin' i t up as I go along end; nd.waiting_for_data_start := true; nd.rx.speed := S100; nd.arb.timer := 0; nd.root.test := false; nd.contend_time := 0; nd.child.count := 0; nd.lowest.unidentified_child := 0; nd.all_child_ports_identif ied := false; nd.self_ID_complete := false; nd.requesting_child := 0; nd.force_root := false; — see above nd.end_of.reception := false; nd.link_req_active := false; nd.arb_enable := false; for i : Portnum do nd.old_connect[i] := false; — actually array of NPORT end; nd.bus_initialize_active := true; nd.gap_count_reset_disable := false; 136 — variables to emulate the physical aspects of a node for i : Portnum do alias pt: nd.ports[i] do p t . ch i ld := false; pt.connected := false; pt.child_ID_complete := false; pt.max_peer_speed := S100; pt.speed.OK := true; pt.data.TPA := Z; pt.data.TPB := Z; end; end; - - current state of the node nd.Pstate := RO; end; end; — set up connection info nodes [0].ports[1].connected := true; nodes[1].ports[0].connected := true; end; — INVARIANTS invariant "Do I manage to get out of state SO?" f o r a l l n: IDnum do nodes[n].Pstate != SI 8c nodes[n].Pstate != S2 end; B.2 L a t e r F i rewi re M o d e l Our work on modeling firewire ended in March 1999. The final model, covering all of the cable physical layer initialization, leaves little room for source level transfor-mation, reflecting the increased Mury experience of the author and feedback from other experienced Mury users. It is included here for archival purposes. — 1394.m — $Id: 1394.m,v 1.32 1999/03/26 00:50:22 bwinters Exp $ — Brian Winters — History: to do: check conditions in All:A0b wrt TIMER_MAX->3? to do: clean up receive_port between states when applicable [nudibranch is a dual UltraSPARC 360MHz, running Solaris] [platypus is a dual UltraSPARC 300MHz, running Solaris] [flake is a dual PII 233MHz, running Linux] 3/25/99 Disabled hack on All:R0b for now. It i sn' t providing a 137 huge improvement over unhacked, and does muck with the model. 5150047 states, 19071094 rules f ired in 852.98s (nudibr) 3/25/99 Added back in a state to my All:R0b hack that is necessary for N=3 to avoid deadlock. 4584064 states, 15338945 rules f ired in 701.40s (nudibr) 3/25/99 Put things back together after playing with N=3 Tested same model as 2/4 on new machine 2907200 states, 9532685 rules f i red in 435.33s (nudibr) 2/04/99 Made All:R0b only apply to states which deadlock without i t 2907200 states, 9532685 rules f ired in 515.88s (platypus) 2/03/99 Removed NPORT from node, made into function 5150047 states, 19071094 rules f ired in 1121.10s (platy) 2/03/99 Commented out a l i t t l e more dead code (A5:A0a, S0:S2) 5150047 states, 19071094 rules f ired in 1071.75s (platy) 2/02/99 Commented out a bunch of dead code (A[2346] are never reached) Added numerous assert/error statements Commented out the asserts 'because they were too slow 5150047 states, 19071094 rules f i red in 1168.31s (pi cnt) 5150047 states, 19071094 rules f i red in 1156.59s (platy) 2/02/99 Removed connected from port, made into function Reordered a couple conditions wrt connectQ Commented out one l ine in one rule (and lost two rule f ir ings) (I think was result of removing old_connect check/update) 5150047 states, 19071094 rules f i red 2/01/99 Took out dead vars and one assignment in self_ID_trans.. . 5150047 states, 19071096 rules f ired in 1206.74s (platy) 2/01/99 Commented out some dead code in self_ID_transmit.actions 5150047 states, 19071096 rules f ired in 1253.60s (platy) 1/15/99 Moved random-hack to only affect x:T3 transitions 5150047 states, 19071096 rules f ired in 1244.00s (platy) 12/01/98 A l l states, two nodes x two ports 5150047 states, 37670446 rules f ired in 2264.98s (platy) 12/01/98 A l l states, no body on A5 or A6, three nodes, each two ports 40-bit hash compression, -m512, "too many active states": 74300000 states, 718279094 rules f ired in 47145.27s (pla) 9940746 states pending 11/30/98 A l l states, no body on A5 or A6 5150047 states, 37670446 rules f i red in 4549.30s (platy) 11/30/98 States R0 through Al implemented, no :A5 or :A6 4343811 states, 31828206 rules f i red in 3275.40s (platy) Pr[even one omitted state] <= 0.000000 Pr[even one undetected error] <= 0.000000 Diameter of reachability graph: 124 11/30/98 States R0 through Al implemented, AO:(!(AOIAl)) not implemented 4343811 states, 31828206 rules f ired in 1617.33s (platy) 11/27/98 States R0 through S3 implemented, S4 p a r t i a l , AO dead ends 1141195 states, 8381326 rules f i red in 518.08s (flake) Pr[even one omitted state] <= 0.000000 Pr[even one undetected error] <= 0.000000 Diameter of reachability graph: 98 11/27/98 States R0 through S3 implemented, S4 dead ends 358971 states, 2638166 rules f ired in 159.42s (flake) Pr[even one omitted state] <= 0.000000 Pr[even one undetected error] <= 0.000000 138 Diameter of reachability graph 11/27/98 States RO through S2 implemented 344211 states, 2533862 rules f Pr[even one omitted state] Pr[even one undetected error] Diameter of reachability graph 11/27/98 States RO through S2 implemented 339171 states, 2498750 rules f Pr[even one omitted state] Pr[even one undetected error] Diameter of reachability graph 11/27/98 States RO through S2 implemented S0:S2 rule never f i r e s , no eff 11/27/98 States RO through SI implemented 218095 states, 1616350 rules f Pr[even one omitted state] Pr[even one undetected error] Diameter of reachability graph 11/27/98 States RO through SO implemented 203695 states, 1519390 rules f Pr[even one omitted state] Pr[even one undetected error] Diameter of reachability graph 11/24/98 States RO through SO implemented 2060216 states, 15204586 rules Pr[even one omitted state] PrCeven one undetected error] Diameter of reachability graph 77 S2 and S4 dead end ired in 149.13s (flake) 114.31s (platypus) <= 0.000000 <= 0.000000 77 no S1:S4, S2 dead ends ired in 147.58s (flake) <= 0.000000 <= 0.000000 77 SI and S2 dead end ective change in model. SI dead ends ired in 89.94s (flake) <= 0.000000 <= 0.000000 71 SO dead ends ired in 82.25s (flake) <= 0.000000 <= 0.000000 71 SO dead ends f i red in 787.31s (flake) <= 0.000000 <= 0.000000 121 const N: 2; HIGHPORT: 1; —HIGHFIF0.DEPTH: 0; TIMER_MAX: 2; number of nodes highest numbered port possible per node highest numbered entry in a FIFO — table 4-32 C0NFIG.TIME0UT: 2; FORCE.ROOT.TIMEOUT: 1; -3; -2: -5; -4: -14; -13; defined as 16384 defined as >=8192 and <= CONFIG TIMEOUT R00T.C0NTEND.FAST: 1; —1; —1; — 2; — defined as 24 R00T_C0NTEND_SL0W: 2; —2; —2; — 3; — defined as 56 RESET_TIME: 1; —3; —5; —14; as 16384 RESET.WAIT: 2; —4; —6; —15; as 16400 MAX_ARB.STATE.TIME: RESET.WAIT; — semi-contrived, GAP.COUNT.MAX: table 4-44 —2; —3; - defined as 63 type IDnum: 0..(N-1); Portnum: 0..HIGHPORT; — FIFOnum: 0..HIGHFIFO.DEPTH; irange: 0..(HIGHPORT+1); PHY.state: enum { RO, R l , TO, T l , T2, T3, SO, SI, S2, S3, S4, 139 AO, A l , A2, A3, A4, A5, A6 }; — bogus types dataBit: boolean; baserate_time: 0..TIMER_MAX; timer: baserate_time; gap_counter: 0..GAP_C0UNT_MAX; —4.4 Cable PHY operation, table 4-37 phyData: enum { L, H, Z }; speedCode: enum { S100, S200, S400 }; portData : record TPA: phyData; TPB: phyData; end; — 4.3.3: transmitted l ine states, table 4-27 ArbLineStateTX: enum { TX.IDLE, TX.REQUEST, TX.GRANT, TX.PARENT.NOTIFY, TX.DATA.PREFIX, TX.CHILD.NOTIFY, TX.IDENT.DONE, TX.DATA.END, TX.BUS.RESET }; — 4.3.3: received l ine states, table 4-28 ArbLineStateRX: enum { RX.IDLE, RX.PARENT.NOTIFY, RX.REQUEST.CANCEL, RX.IDENT.DONE, RX.SELF.ID.GRANT, RX.REQUEST, RX.R00T.C0NTENTI0N, RX.GRANT. RX.PARENT.HANDSHAKE, RX.DATA.END, RX.CHILD.HANDSHAKE, RX.DATA.PREFIX, RX.BUS.RESET }; - PORT definit ion port: record - 4.3.9 Port variables chi ld: boolean; connected: boolean; — replaced with connected(node,port):boolean child.ID.complete: boolean; max.peer.speed: MaxSpeed; —NYM speed.OK: boolean; —NYM data: portData; — this one not exp l i c i t ly defined, guessing here end; - NODE definit ion node: record - 4.3.7 Cable PHY node constants NPORT: irange; PHY.DELAY.CATEGORY: 0( . .3); — this can only be 0 in current spec PHY.SPEED: MaxSpeed; — NYM POWER.CLASS: 0..7; — don't care about physical power characteristics CONTENDER: boolean; - 4.3.8 Node variables, table 4-35 arb.enable: boolean; 140 cable_power_active: boolean; force_root: boolean; gap_count: gap.counter; — guessing on variable type here initiated_reset: boolean; l ink_active: boolean; more_packets: boolean; parent_port: Portnum; physical_ID: IDnum; receive_port: irange; — "transmitting" def: receive_port=NPORT root: boolean; — 4.4 Cable PHY operation, table 4-37 , implied internal variables f ifo_rd_ptr: FIFOnum; fifo_wr_ptr: FIFOnum; FIFO.DEPTH: FIFOnum; FIFO: array [FIFOnum] of dataBit; waiting_for_data_start: boolean; rx_speed: speedCode; arb_timer: timer; root_test: boolean; contend_time: baserate_time; child.count: irange; lowest_unidentified_child: Portnum; al l_child_ports_identif ied: boolean;-self_ID_complete: boolean; requesting_child: Portnum; — potentially need to clean up this one force_root: boolean; — see above end_of.reception: boolean; link_req_active: boolean; arb_enable: boolean; — see above old_connect: array[Portnum] of boolean; — actually array of NPORT bus_init ial ize_active: boolean; gap_count_reset_disable: boolean; — variables implied by the C code or state machines, but never declared cycle_master_req: boolean; fa ir_req: boolean; isoch_req: boolean; imm_req: boolean; end_of.transmission: boolean; — variables to emulate the physical aspects of a node ports: array[Portnum] of port; — current state of the node Pstate: PHY.state; end; var nodes: array[IDnum] of node; — FUNCTIONS — mapping functions, to model the physical wiring — assumes a l l nodes have same number of ports 141 function NP0RT(n: IDnum): irange; begin return HIGHPORT+1; end; — assumes N=2, HIGHP0RT=1 function connected(n: IDnum; port_number: Portnum): boolean; begin — assert (N=2 8: HIGHP0RT=1) "N and/or HIGHPORT do not match"; return ((n=0 & port_number=l) I (n=l & port_number=0)); end; — assumes N=3, HIGHP0RT=1 —function connected(n: IDnum; port_number: Portnum): boolean; --begin — assert (N=3 fc HIGHP0RT=1) "N and/or HIGHPORT do not match"; — return ((n=0 & port_number=l) I (n=l) I (n=2 ft port_number=0)); --end; — assumes N=2, HIGHP0RT=1 function trans_node(n: IDnum; port_number: Portnum): IDnum; begin — assert (N=2 8: HIGHP0RT=1) "N and/or HIGHPORT do not match"; if(n=0 & port_number=l) then return 1; elsif(n=l fc port_number=0) then return 0; else error "Invalid node/port combination"; end; end; — assumes N=3, HIGHP0RT=1 —function trans_node(n: IDnum; port_number: Portnum): IDnum; —begin — assert (N=3 & HIGHP0RT=1) "N and/or HIGHPORT do not match"; if(n=0 k port_number=l) then return 1; elsif(n=l k port_number=0) then return 0; elsif(n=l k port_number=l) then return 2; elsif(n=2 k port_number=0) then return 1; else error "Invalid node/port combination"; end; —end; — assumes N=2, HIGHP0RT=1 function trans_port(n: IDnum; port.number: Portnum): Portnum; begin — assert (N=2 k HIGHP0RT=1) "N and/or HIGHPORT do not match"; if(n=0 k port_number=l) then return 0; els if(n=l k port_number=0) then return 1; else error "Invalid node/port combination"; end; 142 end; — assumes N=3, HIGHP0RT=1 —function trans_port(n: IDnum; port.number: Portnum): Portnum; —begin — assert (N=3 & HIGHP0RT=1) "N and/or HIGHPORT do not match"; if(n=0 _ port_number=l) then return 0; elsif(n=l k port_number=0) then return 1; elsif(n=l & port_number=l) then return 0; elsif(n=2 k port_number=0) then return 1; else error "Invalid node/port combination"; end; —end; — hardware functions, prototyped from table 4-37 —function random_bool(): boolean; —begin pseudorandom - w i l l protocol work even with bad randomizer? return true; return false; return random.value; —end; —procedure portT(n: IDnum; port.number: Portnum; txData: portData); procedure portT(n: IDnum; port.number: Portnum; txData: ArbLineStateTX); begin al ias p: nodes[n].ports[port.number].data do — from table 4-27 switch txData case TX. .IDLE: p.TPA := Z; p.TPB := Z; case TX. .REQUEST: p.TPA := Z; p.TPB := L; case TX. .GRANT: p.TPA := Z; p.TPB := L; case TX. .PARENT.NOTIFY p.TPA := L; p.TPB := Z; case TX. .DATA.PREFIX: p.TPA := L; p.TPB := H; case TX. .CHILD.NOTIFY: p.TPA := H; p.TPB := Z; case TX. .IDENT.DONE: p.TPA := H; p.TPB := Z; case TX. .DATA.END: p.TPA := H; p.TPB := L; 143 case TX.BUS.RESET: p.TPA := H; p.TPB := H; end; end; end; function resolve(a, b: phyData): phyData; begin if(a=Z) then return b; end; if(b=Z I a=b) then return a; end; return Z; end; —function portR(n, port.number: IDnum): portData; function portRCn, port.number: IDnum): ArbLineStateRX; var Tn, Tp: IDnum; otherA, otherB: phyData; begin otherA := Z; otherB := Z; if(connected(n, port.number)) then Tn := trans_node(n, port.number); Tp := trans_port(n, port.number); otherA := nodes[Tn].ports[Tp].data.TPA; otherB := nodes[Tn].ports[Tp].data.TPB; end; al ias pt: nodes[n].ports[port.number].data do — from table 4-28 if(resolve(pt.TPA, otherB) = Z ft resolve(pt.TPB, otherA) = Z) return RX.IDLE; elsif(resolve(pt.TPA, otherB) return RX.PARENT.NOTIFY; — elsif(resolve(pt.TPA, otherB) return RX.IDENT.DONE; elsif(resolve(pt.TPA, otherB) return RX.SELF.ID.GRANT; — elsif(resolve(pt.TPA, otherB) return RX.ROOT.CONTENTION; elsif(resolve(pt.TPA, otherB) return RX.PARENT.HANDSHAKE; elsif(resolve(pt.TPA, otherB) return RX.CHILD.HANDSHAKE; elsif(resolve(pt.TPA, otherB) return RX.DATA.PREFIX; elsif(resolve(pt.TPA, otherB) return RX.BUS.RESET; end; end; end; = Z ft resolve(pt.TPB, otherA) also RX.REQUEST.CANCEL = Z ft resolve(pt.TPB, otherA) = L ft resolve(pt.TPB, also RX.REQUEST = L ft resolve(pt.TPB, — also RX.GRANT = L ft resolve(pt.TPB, — also RX.DATA.END = H ft resolve(pt.TPB, otherA) otherA) otherA) otherA) H ft resolve(pt.TPB, otherA) H ft resolve(pt.TPB, otherA) then L) then H) then Z) then L) then H) then Z) then L) then H) then function portRcomp(n, port.number: IDnum; c: ArbLineStateRX): boolean; var r: ArbLineStateRX; begin r := portR(n, port.number); switch r case RX.PARENT.NOTIFY: i f (c = RX.REQUEST.CANCEL) then return true; end; case RX.SELF.ID.GRANT: 144 i f (c = RX_REQUEST) then return true; end; case RX_ROOT_CONTENTION: i f (c = RX.GRANT) then return true; end; case RX_PARENT_HANDSHAKE: i f (c = RX_DATA_END) then return true; end; end; return (r = c); end; —procedure portTspeed(n, port.number: IDnum; speed: speedCode); —function portRspeedCn, port.number: IDnum): speedCode; function subaction.gap.detect.time(n: IDnum): gap.counter; — table 4-33 begin —defined as: return (28 + (nodes[n].gap.count * 16)); return nodes[n].gap.count / 2; — I HAVE NO JUSTIFICATION FOR THIS CHOICE end; function arb_reset_gap_detect_time(n: IDnum): gap.counter;— table 4-33 begin —defined as: return (28 + (nodes[n].gap.count * 16)); return nodes[n].gap.count; — I HAVE NO JUSTIFICATION FOR THIS CHOICE end; —function ARB_DELAY(n: IDnum): gap.counter; — table 4-34 —begin defined as: return (nodes[n].gap.count * 4); — return nodes[n].gap.count / 2; — HAVE NO JUSTIFICATION FOR THIS CHOICE —end; — 4.4.2.1.2 Bus reset actions and conditions function bus_reset_signal_received(n: IDnum): boolean; — table 4-44 var i : irange; begin i:=0; while(i < NPORT(n)) do if(connected(n, i) k portRcomp(n, i , RX.BUS.RESET)) then return true; end; i:=i+l; end; return false; end; —function connection.state.change(n: IDnum): boolean; — table 4-44 145 —var state_change: boolean; i : irange; —begin state.change := false; — i:=0; — while(i < NPORTCn)) do if(connected(n, i) != nodes[n].old.connect[i]) then state_change := true; nodes[n].old_connect[i] := !nodes[n].old.connect[i]; end; i:=i+l; end; return state_change; —end; procedure reset_start_actions(n: IDnum); — table 4-44 var i : irange; begin nodes[n].root := false; nodes[n].physical_ID := 0; nodes[n].child.count := 0; nodes[n].bus_initialize_active := true; if(nodes[n].gap_count_reset_disable) then nodes[n].gap.count.reset.disable := false; else nodes[n].gap_count := GAP_C0UNT_MAX; —hard coded to 0x3F in table 4-44 end; i:=0; while(i < NPORT(n)) do if(connected(n, i)) then portTCn, i , TX.BUS.RESET); else portTCn, i , TX.IDLE); end; nodes[n].ports[i] .child := false; nodes[n].ports[i].child_ID_complete := false; i:=i+l; end; nodes[n].arb.timer := 0; end; procedure reset_wait_actions(n: IDnum); — table 4-44 var i ; irange; begin i:=0; while(i < NPORT(n)) do portTCn, i , TX.IDLE); i:=i+l; end; nodes[n].arb.timer := 0; end; function reset.completeCn: IDnum): boolean; — table 4-44 var i : irange; begin i:=0; whileCi < NPORTCn)) do ifCconnectedCn, i) & IportRcompCn, i , RX.IDLE) & IportRcompCn, i , RX.PARENT.NOTIFY)) then return false; 146 end; i:=i+l; end; return true; end; function arb_state_timeout(n: IDnum): boolean; — support for figure 4-22 begin al ias nd: nodes[n] do alias st: nd.Pstate do return ((st != Rl) & (st != AO) & (st != A5) fc (st != A6) & (nd.arb.timer >= MAX.ARB.STATE.TIME)); end; end; end; — 4.4.2.2.2 Tree-ID actions and conditions procedure tree .ID.s tart .act ions . interp. l (n: IDnum); — table 4-45 var i , temp.count: irange; begin nodes[n].arb_timer := 0; — LOOP FOREVER??? EXCUSE ME???? — my suspicion here is that they intend that this be going on as some — sort of background process that is always updating child count, but — on second thought that doesn't make sense, because we immediately go — into a reset state i f our connections change while(true) do temp.count := 0; i:=0; while(i<NP0RT(n)) do — formatting of standard is ambiguous here; using C code and not indention — my suspicion is that this interpretation is WRONG, but we'l l see if(!connected(n, i) I portRcomp(n, i , RX.PARENT.NOTIFY)) then nodes[n].ports[i] .child := true; temp.count := temp.count + 1; nodes[n].child.count := temp.count; end; i:=i+l; end; end; end; procedure tree_ID_start_actions_interp_2(n: IDnum); — table 4-45 var i , temp.count: irange; begin nodes[n].arb.timer := 0; temp.count := 0; i:=0; while(i<NP0RT(n)) do — formatting of standard is ambiguous here; using indention and not C code if(!connected(n, i) I portRcomp(n, i , RX.PARENT.NOTIFY)) then nodes[n].ports[i] .child := true; temp.count := temp.count + 1; end; i:=i+l; end; nodes [n].child.count := temp.count; end; end; 147 procedure tree_ID_start_actions(n: IDnum); — table 4-45 begin tree_ID_start_actions_interp_l(n); tree_ID_start.actions.interp_2(n); end; procedure child_handshake_actions(n: IDnum); - - table 4-45 var i : irange; begin nodes[n].root := true; i:=0; while(i < NPORT(n)) do if(connected(n, i)) then if(nodes[n].ports[i] .child) then portT(n, i , TX_CHILD_NOTIFY); else portT(n, i , TX_PARENT_NOTIFY); nodes[n].parent_port := i ; nodes[n].root := false; end; end; i:=i+l; end; end; function child_handshake_complete(n: IDnum): boolean; — table 4-45 var i : irange; begin •i:=0; while(i < NPORT(n)) do if(nodes[n] .ports[ i ] .chi ld & connected(n, i) k !portRcomp(n, i , RX.CHILD.HANDSHAKE)) then return false; end; i:=i+l; end; return true; end; procedure root_contend_actions(n: IDnum; r : boolean); — table 4-45 var i : irange; begin if(random_bool()) then i f ( r ) then nodes[n].contend.time := R00T_C0NTEND_SL0W; else nodes[n].contend_time := R00T_C0NTEND_FAST; end; i:=0; while(i < NPORT(n)) do if(nodes[n].ports[i] .child) then portT(n, i , TX.CHILD.NOTIFY); else portT(n, i , TX.IDLE); end; i:=i+l; end; nodes[n].arb_timer := 0; 148 end; procedure self_ID_start_actions(n: IDnum); — table 4-46 var i : irange; begin nodes[n] .a l l .chi ld .ports . ident i f ied := true; i:=0; vhi leCi < NPORT(n)) do if(nodes[n].ports[i].child_ID_complete) then portTCn, i , TX_DATA_PREFIX); else portTCn, i , TX_IDLE); i fCnodes[n].ports[i] .child & connectedCn, i ) ) then ifCnodes[n].all_child_ports_identified) then nodes[n].lowest.unidentified.child := i ; end; nodes[n].all_child_ports_identified := false; end; end; i:=i+l; end; end; procedure self_ID_grant_actionsCn: IDnum); — table 4-46 var i : irange; begin i:=0; whileCKNPORTCn)) do ifC!nodes[n].all_child_ports_identified & Ci = nodes[n].lowest.unidentified.child)) then portTCn, i , TX_GRANT); else portTCn, i , TX.DATA.PREFIX); end; i:=i+l; end; end; procedure self_ID_receive_actionsCn: IDnum); — table 4-46 var i : irange; begin portTCn, nodes[n].receive_port, TX_IDLE); — — receive_actionsCn); nodes[n].physical.ID := nodes[n].physical_ID + 1; i:=0; whileCKNPORTCn)) do portTCn, i , TX.IDLE); i:=i+l; end; end; procedure self_ID_transmit_actionsCn: IDnum); — table 4-46 var port.number: irange; — port.number: 0..1024; last .SID.pkt, SID_pkt.number: irange; begin — last.SID.pkt := CNPORTCn) + 4) / 8; port .number := 0; nodes[n].self.ID.complete := false; nodes[n].receive.port := NPORTCn); — this is def for "transmitV 149 —start_tx_packet(n, S100); — I've abstracted away everying about doing the SID packets, which make — this loop pretty meaningless SID.pkt.number := 0; - - while(SID_pkt_number <= last_SID_pkt) do — abstracting away SID packet construction THIS SECTION CAUSES PORT NUMBER TO GO OUT OF RANGE. AT BEST THIS IS JUST BAD PRACTICE. AT WORST IT IS VERY BAD. Let's give them enough rope to hang themselves. Alan and I later looked this over, and the stuff I'm abstracting away handles this properly. Why they did this was s t i l l a myster while(port_number < ((SID_pkt_number + 1)*8 - 5)) do — abstracting away more SID packet construction port.number :=port_number+l; end; — abstracting away even more SID packet construction — if(SID.pkt.number = last.SID.pkt) then — don't send quadlets stop_tx_packet(n, TX_DATA_END, S100); else stop_tx_packet(n, TX.DATA.PREFIX, S100); end; SID_pkt.number:=SID_pkt_number+l; end; port.number:=0; while(port.number < NPORT(n)) do if(port.number = nodes[n].parent.port) then portT(n, port.number, TX.IDENT.DONE); — portTspeedO; — wait.time(); — portTspeedO ; — PH.EVENT.ind(SELF_ID_COMPLETE, physical.ID, root); else portT(n, port.number, TX.IDLE); end; port.number:=port_number+l; — bad bug in standard I think upon further ref lect ion, I have no idea why I thought this end; nodes[n].self.ID.complete := true; end; —function child_request(n: IDnum): boolean; — table 4-47 —var i : irange; —begin al ias nd: nodes[n] do — i:=0; — while(i < NPORT(n)) do if(connected(n, i ) _ nd.ports [ i ] .chi ld & portRcomp(n, i , RX.REQUEST)) then nd.requesting.child := i ; return true; end; i:=i+l; end; return false; —end; end; function data_coming(n: IDnum): boolean; — table 4-47 var i : irange; begin al ias nd: nodes[n] do 150 i:=0; while(i < NPORT(n)) do if(connected(n, i) fc portRcomp(n, i , RX_DATA_PREFIX)) then nd.receive_port := i ; return true; end; i:=i+l; end; return false; end; end; procedure idle_actions(n: IDnum); — table 4-47 var i : irange; begin i:=0; while(i < NPORT(n)) do portT(n, i , TX.IDLE); i:=i+l; end; end; procedure subaction.detect.actions(n: IDnum); — table 4-47 begin —PH.DATA.ind(SUBACTION.GAP); i f (nodes[n] .bus. init ial ize .act ive) then — PH.EVENT.ind(BUS.RESET.COMPLETE); nodes[n] .bus. init ial ize.active := false; end; end; —procedure request_delay_actions(n: IDnum); — table 4-47 —begin nodes[n].arb.timer := 0; nodes[n].l ink.req.active := true; —end; —procedure request_actions(n: IDnum); — table 4-47 —var i : irange; —begin al ias nd: nodes[n] do — i:=0; — while(i<NP0RT(n)) do if(connected(n, i) fc nd.ports[ i ] .chi ld fc (nd.l ink.req.active I ( i != nd.requesting.child))) then portT(n, i , TX.DATA.PREFIX); end; i:=i+l; end; — portT(n, nd.parent.port, TX.REQUEST); —end; end; —procedure grant_actions(n: IDnum); — table 4-47 —var i : irange; —begin — i:=0; — while(i < NPORT(n)) do i f ( i = nodes[n].requesting.child) then portT(n, i , TX.GRANT); elsif(connected(n, i ) & nodes[n].ports[i].child) then portT(n, i , TX.DATA.PREFIX); end; 151 i:=i+l; end; —end; procedure receive_actions(n: IDnum); — table 4-47 var — i : this one isn't irange; — bit.count: ???; phy_pkt: some real ly big union; test_end, received_data: boolean; good_phy.packet: boolean; begin al ias nd: nodes[n] do —bit.count := 0; —test.end := false; —nd. fa ir .req := false; --nd.cycle_master_req := false; —PHY_DATA.ind(DATA_PREFIX); —nd.rx_speed := start_rx_packet(); —PHY.DATA.ind(DATA_START(rx_speed)); —while(!test_end) do rx_bit(&received_data, &test_end); if(!test_end) then PH_DATA.ind(received.data); if(bit_count < 64) then phy_pkt.bits[bit_count++] = received_data; end; end; —end; —if(portRcomp(n, nd.receive_port, RX_DATA_PREFIX)) then — PH.DATA. ind(DATA_PREFIX) ; —elsif(portRcomp(n, nd.receive.port, RX_DATA_END)) then — PH.DATA.ind(DATA.END); —end; —stop_rx_packet(ending_data); nd.end_of.reception := true; i f ( bit_count = 64 true ) then good_phy.packet := true; — i:=0; - - while(i<32) do good.phy.packet := compare bits in 1st half vs the negated 2nd half end; if(good_phy_packet) then phy_addr := received.bits; and a bunch of other stuff I'm not going to model at this point end; end; end; end; —procedure transmit_actions(n: IDnum); — table 4-47 —var — i : why did they declare i t? test_end: boolean; data_to_transmit: phyData; —begin al ias nd: nodes[n] do test_end := false; nd.imm_req := false; i f (nd.fair_req) then nd.arb_enable := false; nd.fair_req := false; 152 end; nd.cycle_master_req := false; nd.isoch_req := false; — nd.receive_port := NPORT(n); — we are transmitting start_tx_packet(req_speed); while(!test_end) do a bunch of stuff I'm not going to model yet end; nd.end_of.transmission := true; --end; end; procedure change_PHY_state_withrand(n: IDnum; r: boolean; newstate: PHY_state); begin assert newstate=T3 "Using rand change_PHY on inval id state change"; nodes[n].Pstate := newstate; switch newstate case T3: root_contend_actions(n, r ) ; - - figure 4-23 end; end; procedure change_PHY_state(n: IDnum; newstate: PHY.state); begin — assert newstate!=T3 "Using nonrand change_PHY on inval id state change" nodes[n].Pstate := newstate; switch newstate case RO: reset_start_actions(n); — figure 4-22 case R l : reset_wait_actions(n); — figure 4-22 case TO: tree_ID_start_actions(n); — figure 4-23 case T l : child_handshake_actions(n); — figure 4-23 case T2: — this state is just a waiting point (figure 4-23) — case T3: root_contend_actions(n, r ) ; — figure 4-23 case SO: self_ID_start_actions(n); — figure 4-24 case SI: self_ID_grant_actions(n); — figure 4-24 case S2: self_ID_receive_actions(n); — f ig ire 4-24 case S3: — a l l output at this state is on transitions — figure 4-24 case S4: self_ID_transmit_actions(n); — figure 4-24 case AO: idle_actions(n); — figure 4-25 case A l : — this state doesn't actually do anything (figure 4-25, 4.4.2.4.1) case A2: error "Transition to state A2"; request_delay_actions(n); — figure 4-25 case A3: error "Transition to state A3"; request_actions(n); — figure 4-25 case A4: 153 error "Transition to state A4"; grant.actions(n); — figure 4-25 case A5: receive_actions(n); — figure 4-25 case A6: error "Transition to state A6"; transmit_actions(n); — figure 4-25 end; end; — RULESETS — random value hack --ruleset r: boolean do - - state machine by node ruleset n: IDnum do alias nd: nodes[n] do al ias st: nd.Pstate do rule "increment timer (modeling hack)" ((st != Al) & — Al "takes no time" (nd.arb.timer < TIMER.MAX)) ==> begin nd.arb.timer := nd.arb.timer + 1; end; rule "Transition All:R0a (4.4.2.1.1)" bus_reset_signal_received(n) ==> begin — PH.STATE.ind(BUS_RESET_START) (4.4.2.1) nd.initiated_reset := false; change_PHY_state(n, RO); end; experiment to see how bad deadlock is without the timeout rule "Transition All:R0b (4.4.2.1.1)" ( ( (st=T2 I st=T3 I st=S4 I st=S0) fe — statespace reduction hack — this may not be va l id <==== arb_state_timeout(n)) —I PH_CONT.req(bus_reset) I connection_state_change(n) ) ==> begin — PH_STATE.ind(BUS_RESET_START) (4.4.2.1) nd.initiated_reset := true; change_PHY_state(n, RO); end; rule "Transition R0:R1 (4.4.2.1.1)" ((st = RO) fe (nd.arb.timer >= RESET.TIME)) ==> begin change_PHY_state(n, Rl ) ; end; rule "Transition R1:R0 (4.4.2.1.1)" ((st = Rl) fe (nd.arb.timer >= RESET.WAIT)) ==> begin change_PHY_state(n, RO); 154 end; rule "Transition R1:T0 (4.4.2.1.1)" ((st = Rl) & reset_complete(n)) ==> begin change_PHY_state(n, TO); end; - this was never happening, so we can speed things up by removing i t - rule "Transition T0:T0 (4.4.2.2.1)" ((st = TO) & ((nd.arb.timer >= CONFIG.TIMEOUT) & (nd.child.count < (NPORT(n) - 1)))) ==> begin — signal PH.STATE.ind(CONFIG.TIMEOUT) (4.4.2.2) change_PHY_state(n, TO); end; rule "Transition T0:T1 (4.4.2.2.1)" ((st = TO) & ((nd.child.count = NPORT(n)) I (((nd.force.root fc (nd.arb.timer >= FORCE.ROOT.TIMEOUT))I (!nd.force.root fc (nd.arb.timer >= 0))) fc (nd.child.count = (NPORT(n) - 1))))) ==> begin change_PHY_state(n, T l ) ; end; rule "Transition T1:T2 (4.4.2.2.1)" ((st = Tl) & child.handshake.complete(n)) ==> begin change_PHY_state(n, T2); end; rule "Transition T2:S0 (4.4.2.2.1)" ((st = T2) fc (nd.root I portRcomp(n, nd.parent.port, RX.PARENT.HANDSHAKE))) ==> begin change_PHY_state(n, SO); end; ruleset r: boolean do rule "Transition T2:T3 (4.4.2.2.1)" ((st = T2) & portRcomp(n, nd.parent.port, RX.ROOT.CONTENTION)) ==> begin change_PHY_state_withrand(n, r , T3); end; end; rule "Transition T3:T2 (4.4.2.2.1)" ((st = T3) & (portRcomp(n, nd.parent.port, RX.IDLE) fc (nd.arb.timer > nd.contend.time))) ==> begin portT(n, nd.parent.port, TX.PARENT.NOTIFY); — 4.4.2.2 change_PHY_state(n, T2); end; rule "Transition T3:T1 (4.4.2.2.1)" ((st = T3) & (portRcomp(n, nd.parent.port, RX.PARENT.NOTIFY) fc (nd.arb.timer > nd.contend.time))) ==> begin — 4.4.2.2: "node is now root" nd.ports[nd.parent.port].child := true; change.PHY_state(n, T l ) ; end; rule "Transition S0:S1 (4.4.2.3.1)" ((st = SO) & (nd.root I portRcomp(n, nd.parent.port, RX.SELF.ID.GRANT))) ==> begin change.PHY_state(n, S l ) ; 155 end; this was never happening, so speed things up by removing i t rule "Transition S0:S2 (4.4.2.3.1)" ((st = SO) ft portRcomp(n, nd.parent.port, RX.DATA.PREFIX)) ==> begin nd.receive.port := nd.parent.port; change_PHY_state(n, S2); end; rule "Transition S1:S2 (4.4.2.3.1)" ((st = Sl) ft portRcomp(n, nd.lowest.unidentified_child, RX_DATA_PREFIX)) ==> begin nd.receive_port := nd.lowest_unidentified.child; change_PHY_state(n, S2); end; rule "Transition S1:S4 (4.4.2.3.1)" ((st = Sl) ft nd .a l l . ch i ld .ports . ident i f i ed) ==> begin — nd.ports[nd.parent.port].max.peer.speed := S100; change_PHY_state(n, S4); end; rule "Transition S2:S0a (4.4.2.3.1)" ((st = S2) ft (portRcomp(n, nd.receive_port, RX.IDLE) I portRcomp(n, nd.receive.port, RX.SELF.ID.GRANT))) begin change_PHY_state(n, SO); end; rule "Transition S2:S0b (4.4.2.3.1)" ((st = S2) ft ( PHY.SPEED = S100 ft portRcomp(n, nd.receive_port, RX_IDENT_DONE))) ==> begin nd.ports[nd.receive_port].child_ID_complete := true; change_PHY_state(n, SO); end; •rule "Transition S2:S3 (4.4.2.3.1)" • ((st = S2) ft (PHY.SPEED != S100 ft portRcomp(n, nd.receive.port, RX_IDENT_DONE)) ==> begin nd.ports[nd.receive.port].child.ID.complete := true; portTspeed(n, nd.receive.port, PHY.SPEED); nd.ports[nd.receive.port].max.peer.speed := S100; nd.arb.timer := 0; change_PHY_state(n, S3); end; •rule "Transition S3:S0 (4.4.2.3.1)" • ((st = S3) & (arb.timer >= SPEED.SIGNAL.LENGTH)) ==> begin portTspeed(n, nd.receive.port, S100); change_PHY_state(n, SO); end; •rule "Transition S3:S3a (4.4.2.3.1)" • ((st = S3) ft (portRspeed(n, nd.receive.port) = S200)) ==> begin nd.ports[nd.receive.port].max.peer.speed := S200; change_PHY_state(n, S3); end; •rule "Transition S3:S3b (4.4.2.3.1)" • ((st = S3) ft (portRspeed(n, nd.receive.port) = S400)) ==> begin 156 nd.ports[nd.receive.port].max.peer.speed := S400; change_PHY_state(n, S3); end; rule "Transition S4:S4a (4.4.2.3.1)" • ((st = S4) fc (portRspeed(n, nd.parent.port) = S200)) ==> begin nd.ports [nd.parent.port].max.peer.seed := S200; change_PHY_state(n, S4); end; •rule "Transition S4:S4b (4.4.2.3.1)" • ((st = S4) & (portRspeed(n) = S400)) ==> begin nd.ports[nd.parent.port].max.peer.seed := S400; change_PHY_state(n, S4); end; rule "Transition S4:A0 (4.4.2.3.1)" ((st = S4) & (nd.self.ID.complete & (nd.root I portRcomp(n, nd.parent.port, RX.DATA.PREFIX)))) == begin change_PHY_state(n, AO); end; •rule "Transition A0:A0a (4.4.2.4.1)" • ((st = AO) & (PH.ARB.req(CYCLE_MASTER, req.speed))) ==> begin nd.cycle.master.req':= true; change_PHY_state(n, AO); end; •rule "Transition A0:A0b (4.4.2.4.1)" • ((st = AO) fc (PH.ARB.req(FAIR, req.speed))) ==> begin nd . fa i r . req := true; change_PHY_state(n, AO); end; •rule "Transition A0:AOc (4.4.2.4.1)" • ((st = AO) & (PH.ARB.req(IS0CH, req.speed))) ==> begin nd.isoch.req := true; change_PHY_state(n, AO); end; rule "Transition A0:Ala (4.4.2.4.1)" ((st = AO) & (nd.arb.timer = subaction.gap.detect.time(n))) ==> begin subaction.detect.actions(n); change_PHY_state(n, A l ) ; end; rule "Transition A0:Alb (4.4.2.4.1)" ((st = AO) & (nd.arb.timer = arb.reset_gap_detect.time(n))) ==> begin nd.arb.enable := true; PH.DATA.ind(ARB_RESET_GAP); change_PHY_state(n, A l ) ; end; • this was never occuring, so speed things up • rule "Transition A0:A2 (4.4.2.4.1)" ((st = AO) & ((nd.arb.timer > arb_reset_gap_detect_time(n)) fc 1 (nd.cycle.master.req I (nd.fair .req & nd.arb.enable)))) ==> begin change_PHY_state(n, A2); 157 end; this was never occuring, so speed things up rule "Transition A0:A3 (4.4.2.4.1)" ((st = AO) ft ((child_request(n) I nd.isoch_req) ft Ind.root begin change_PHY_state(n, A3); end; this was never occuring, so speed things up rule "Transition A0:A4 (4.4.2.4.1)" ((st = AO) & (child_request(n) & nd.root)) ==> begin change_PHY_state(n, A4); end; rule "Transition A0:A5 (4.4.2.4.1)" ((st = AO) fc data_coming(n)) ==> begin i f (nd. fa ir_req I nd.cycle_master_req) then PHY_.ARB.conf (LOST) ; end; change_PHY_state(n, A5); end; this was never occuring, so speed things up rule "Transition A0:A6 (4.4.2.4.1)" ((st = AO) & (nd.imm_req I (nd.root & nd.isoch_req))) ==> begin PHY_ARB.conf(WON); change_PHY_state(n, A6); end; rule "Transition A1:A0 (4.4.2.4.1)" ((st = Al) & ! (nd.cycle_master_req I (nd.fair_.req & nd.arb_enable)) ) ==> begin change_PHY_state(n, AO); end; this was never occuring, so speed things up rule "Transition A1:A2 (4.4.2.4.1)" ((st = Al) & (nd.cycle_raaster_req I (nd.fair_req ft nd.arb.enable))) ==> begin . change_PHY_state(n, A2); end; this was never occuring, so speed things up rule "Transition A2:A3 (4.4.2.4.1)" ((st = A2) ft ((nd.arb.timer > ARB.DELAY(n)) ft Ind.root)) = begin change_PHY_state(n, A3); end; this was never occuring, so speed things up rule "Transition A2:A5 (4.4.2.4.1)" ((st = A2) ft data_coming(n)) ==> begin PHY.ARB.conf(LOST); nd.link_req_active := false; change_PHY_state(n, A5); end; this was never occuring, so speed things up rule "Transition A3:A0 (4.4.2.4.1)" ((st = A3) fc (portRcomp(n, nd.parent_port, RX.GRANT) & !nd.link_req_active ft !child_request(n))) ==> 158 begin change_PHY_state(n, AO); end; this was never occuring, so speed things up rule "Transition A3:A4 (4.4.2.4.1)" ((st = A3) 8c (portRcomp(n, nd .parent .port , RX.GRANT) 8c child.request(n))) ==> begin change_PHY_state(n, A4); end; this was never occuring, so speed things up rule "Transition A3:A5 (4.4.2.4.1)" ((st = A3) k (portRcomp(n, nd.parent.port, RX.GRANT) & !nd. link_req_active 8k ! child_request (n) ) ) ==> begin change_PHY_state(n, A5); end; this was never occuring, so speed things up rule "Transition A3:A6 (4.4.2.4.1)" ((st = A3) 8k (portRcomp(n, nd.parent.port, RX.GRANT) 8k (nd.link_req_active I nd.isoch.req))) ==> begin PHY.ARB. conf (WON) ; change_PHY_state(n, A6); end; this was never occuring, so speed things up rule "Transition A4:A0 (4.4.2.4.1)" ((st = A4) k portRcomp(n, nd.requesting.child, RX.REQUEST.CANCEL)) ==> begin nd.arb.timer := 0; change_PHY_state(n, AO); end; this was never occuring, so speed things up rule "Transition A4:A5 (4.4.2.4.1)" ((st = A4) k data.coming(n)) ==> begin change_PHY_state(n, A5); end; this was never occuring, so speed things up rule "Transition A5:A0a (4.4.2.4.1)" ((st = A5) 8c (nd.end.of.reception 8c portRcomp(n, nd.receive.port, RX.DATA.END))) begin nd.arb.timer := 0; change_PHY_state(n, AO); end; rule "Transition A5:A0b (4.4.2.4.1)" ((st = A5) 8c portRcomp(n, nd.receive.port, RX.IDLE)) ==> begin nd.arb.timer := 0; change_PHY_state(n, AO); end; rule "Transition A5:A5a (4.4.2.4.1)" ((st = A5) 8fc (nd.end.of.reception 8c portRcomp(n, nd.receive.port, RX.DATA.PREFIX))) begin change_PHY_state(n, A5); end; -rule "Transition A5:A5b (4.4.2.4.1)" 159 — ((st = A5) & PH.ARB.req(IMMEDIATE, req.speed)) ==> begin nd.imm.req := true; change_PHY_state(n, A5); end; - -ru le "Transition A5:A5c (4.4.2.4.1)" - - ((st = A5) _ PH.ARB.req(IS0CH, req.speed)) ==> begin nd.isoch.req := true; change.PHY_state(n, A5); end; — this was never occuring, so speed things up rule "Transition A6:A0 (4.4.2.4.1)" ((st = A6) & nd.end.of.transmission) ==> begin nd.arb.timer := 0; change_PHY_state(n, AO); end; state machine by node - random value — INITIALIZATION CODE startstate begin for n: IDnum do alias nd: nodes[n] do - - 4.3.7 Cable PHY node constants nd.NPORT := HIGHPORT + 1; nd.PHY.DELAY.CATEGORY := 0; — this can only be 0 in current spec nd.PHY.SPEED := S100; — NYM nd.POWER.CLASS := 0; — don't care about phys power characteristics nd.CONTENDER := false; — don't want to model resource manager role — 4.3.8 Node variables, table 4-35 nd.arb.enable := false; nd.cable.power.active := true; nd.force.root := false; — not going to model this yet nd.gap.count := GAP.COUNT.MAX; nd.init iated.reset := false; — should add some rules to allow a — node to choose to in i t ia te reset at — any time nd l ink.act ive := false; nd more.packets : = false nd parent.port := 0; nd physical.ID := 0; nd receive.port : = 0; nd root := false; — 4.4 Cable PHY operation, table 4-37, implied internal variables nd . f i fo . rd .p tr := 0; nd.f i fo .wr.ptr := 0; nd.FIFO.DEPTH := HIGHFIFO.DEPTH; for i : FIFOnum do nd.FIF0[i] := false; — just makin' i t up as I go along end; 160 nd.waiting_for_data_start := true; nd.rx_speed := S100; nd.arb.timer := 0; nd.root_test := false; nd.contend_time := 0; nd.child.count := 0; nd.lowest.unidentified.child := 0; nd.all_child_ports_identified := false; nd. self_ID_complete := false; nd.requesting.child := 0; nd.force_root := false; — see above nd.end.of.reception := true; nd.link_req_active := false; nd.arb_enable := false; — redundant, see above for i : Portnum do nd.old.connect[i] := false; — actually array of NPORT end; nd.bus_initialize_active := true; nd.gap_count_reset_disable := false; variables implied by the C code or state machines, but never declared nd.cycle_master_req := false; nd.fair_req := false; nd.isoch_req := false; nd.imm_req := false; nd.end_of.transmission := true; variables to emulate the physical aspects of a node for i : Portnum do alias pt: nd.ports[i] do pt.child := false; pt.connected := false; pt.child_ID_complete := false; pt.max_peer_speed := S100; pt.speed_.0K := true; pt.data.TPA := Z; pt.data.TPB := Z; end; end; current state of the node nd.Pstate := R0; end; end; set up connection info — no longer use this method, see connectedO assumes N=2, HIGHP0RT=1 nodes[0].ports[1].connected := true; nodes[1].ports[0].connected := true; assumes N=3, HIGHP0RT=1 nodes[0].ports[1].connected := true; nodes[1].ports[0].connected := true; nodes[1].ports[1].connected := true; nodes[2].ports[0].connected := true; end; INVARIANTS 161 invariant "Do I stay within the expected states?" f o r a l l n: IDnum do nodes[n].Pstate != S3 & — nodes[n].Pstate != Al nodes[n].Pstate != A2 _ nodes[n].Pstate != A3 k nodes [n] .Pstate != A4 8c nodes [n] .Pstate != A6 end; 162 

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

Usage Statistics

Share

Embed

Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                        
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            src="{[{embed.src}]}"
                            data-item="{[{embed.item}]}"
                            data-collection="{[{embed.collection}]}"
                            data-metadata="{[{embed.showMetadata}]}"
                            data-width="{[{embed.width}]}"
                            async >
                            </script>
                            </div>
                        
                    
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:
https://iiif.library.ubc.ca/presentation/dsp.831.1-0051531/manifest

Comment

Related Items