File: Model.cc

package info (click to toggle)
rumur 2020.12.20-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye
  • size: 3,292 kB
  • sloc: cpp: 17,090; ansic: 2,537; objc: 1,542; python: 1,120; sh: 538; yacc: 536; lex: 229; lisp: 15; makefile: 5
file content (132 lines) | stat: -rw-r--r-- 3,472 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
#include <algorithm>
#include <cassert>
#include <cstddef>
#include <cstdint>
#include <gmpxx.h>
#include "location.hh"
#include <memory>
#include <rumur/Decl.h>
#include <rumur/except.h>
#include <rumur/Function.h>
#include <rumur/indexer.h>
#include <rumur/Model.h>
#include <rumur/Node.h>
#include <rumur/Property.h>
#include <rumur/Ptr.h>
#include <rumur/Rule.h>
#include <rumur/traverse.h>
#include <rumur/TypeExpr.h>
#include <string>
#include <unordered_set>
#include <vector>

namespace rumur {

Model::Model(const std::vector<Ptr<Decl>> &decls_,
    const std::vector<Ptr<Function>> &functions_,
    const std::vector<Ptr<Rule>> &rules_, const location &loc_):
    Node(loc_) {

  children.reserve(decls_.size() + functions_.size() + rules_.size());
  children.insert(children.end(), decls_.begin(), decls_.end());
  children.insert(children.end(), functions_.begin(), functions_.end());
  children.insert(children.end(), rules_.begin(), rules_.end());
}

Model::Model(const std::vector<Ptr<Node>> &children_, const location &loc_):
  Node(loc_), children(children_) { }

Model *Model::clone() const {
  return new Model(*this);
}

mpz_class Model::size_bits() const {
  mpz_class s = 0;
  for (const Ptr<Node> &n : children) {
    if (auto v = dynamic_cast<const VarDecl*>(n.get()))
      s += v->type->width();
  }
  return s;
}

void Model::validate() const {

  // Check all state variable names are distinct.
  {
    std::unordered_set<std::string> names;
    for (const Ptr<Node> &c : children) {
      if (auto v = dynamic_cast<const VarDecl*>(c.get())) {
        if (!names.insert(v->name).second)
          throw Error("duplicate state variable name \"" + v->name + "\"",
            v->loc);
      }
    }
  }
}

void Model::visit(BaseTraversal &visitor) {
  visitor.visit_model(*this);
}

void Model::visit(ConstBaseTraversal &visitor) const {
  visitor.visit_model(*this);
}

mpz_class Model::liveness_count() const {

  // Define a traversal for counting liveness properties.
  class LivenessCounter : public ConstTraversal {

   public:
    mpz_class count = 0;
    mpz_class multiplier = 1;

    void visit_ruleset(const Ruleset &n) final {
      /* Adjust the multiplier for the number of copies of the contained rules
       * we will eventually generate.
       */
      for (const Quantifier &q : n.quantifiers) {
        assert (q.constant() && "non-constant quantifier in ruleset");

        multiplier *= q.count();
      }

      // Descend into our children; we can ignore the quantifiers themselves.
      for (const Ptr<Rule> &r : n.rules)
        dispatch(*r);

      /* Reduce the multiplier, removing our effect. This juggling is necessary
       * because we ourselves may be within a ruleset or contain further
       * rulesets.
       */
      for (const Quantifier &q : n.quantifiers) {
        assert(multiplier % q.count() == 0 && "logic error in handling "
          "LivenessCounter::multiplier");

        multiplier /= q.count();
      }
    }

    void visit_propertyrule(const PropertyRule &n) final {
      if (n.property.category == Property::LIVENESS)
        count += multiplier;
      // No need to descend into child nodes.
    }

    virtual ~LivenessCounter() = default;
  };

  // Use the traversal to count liveness rules.
  LivenessCounter lc;
  lc.dispatch(*this);

  return lc.count;
}

void Model::reindex() {
  // Re-number our and our children's 'unique_id' members
  Indexer i;
  i.dispatch(*this);
}

}