Grcov report - data

1

use std::cell::RefCell;

2

use std::mem::ManuallyDrop;

3

4

use merc_aterm::Symb;

5

use merc_aterm::Symbol;

6

use merc_aterm::SymbolRef;

7

use merc_aterm::Term;

8

use merc_aterm::is_int_term;

9

10

thread_local! {

11

    /// Thread local storage that stores various default terms representing data symbols.

12

    pub static DATA_SYMBOLS: RefCell<DataSymbols> = RefCell::new(DataSymbols::new());

13

14

15

/// Defines default symbols and terms for data elements.

16

///

17

/// These mirror the mCRL2 definitions since that is convenient for loading the mCRL2 binary formats.

18

///

19

/// All `Symbol` fields are wrapped in `ManuallyDrop` so that their destructors never run at thread

20

/// exit.

21

pub struct DataSymbols {

22

    // Sorts

23

    pub basic_sort_symbol: ManuallyDrop<Symbol>,

24

    pub function_sort_symbol: ManuallyDrop<Symbol>,

25

    pub container_sort_symbol: ManuallyDrop<Symbol>,

26

    pub structured_sort_symbol: ManuallyDrop<Symbol>,

27

    pub untyped_sort_symbol: ManuallyDrop<Symbol>,

28

    pub untyped_possible_sorts_symbol: ManuallyDrop<Symbol>,

29

30

    // Data expressions that are abstractions

31

    pub data_binder_symbol: ManuallyDrop<Symbol>,

32

    pub data_lambda_symbol: ManuallyDrop<Symbol>,

33

    pub data_exists_symbol: ManuallyDrop<Symbol>,

34

    pub data_forall_symbol: ManuallyDrop<Symbol>,

35

    pub data_set_comprehension_symbol: ManuallyDrop<Symbol>,

36

    pub data_bag_comprehension_symbol: ManuallyDrop<Symbol>,

37

    pub data_untyped_set_bag_comprehension_symbol: ManuallyDrop<Symbol>,

38

39

    // Data expressions

40

    pub data_function_symbol: ManuallyDrop<Symbol>,

41

    pub data_function_symbol_no_index: ManuallyDrop<Symbol>,

42

    pub data_variable: ManuallyDrop<Symbol>,

43

    pub data_where_clause: ManuallyDrop<Symbol>,

44

    pub data_untyped_identifier_clause: ManuallyDrop<Symbol>,

45

46

    /// The data application symbol for a given arity.

47

    data_appl: Vec<Symbol>,

48

49

50

impl DataSymbols {

51

1164

    fn new() -> Self {

52

1164

        Self {

53

1164

            basic_sort_symbol: ManuallyDrop::new(Symbol::new("SortId", 1)),

54

1164

            function_sort_symbol: ManuallyDrop::new(Symbol::new("SortArrow", 2)),

55

1164

            container_sort_symbol: ManuallyDrop::new(Symbol::new("SortCons", 2)),

56

1164

            structured_sort_symbol: ManuallyDrop::new(Symbol::new("SortStruct", 1)),

57

1164

            untyped_sort_symbol: ManuallyDrop::new(Symbol::new("UntypedSortUnknown", 0)),

58

1164

            untyped_possible_sorts_symbol: ManuallyDrop::new(Symbol::new("UntypedSortsPossible", 1)),

59

1164

60

1164

            data_binder_symbol: ManuallyDrop::new(Symbol::new("Binder", 3)),

61

1164

            data_lambda_symbol: ManuallyDrop::new(Symbol::new("Lambda", 0)),

62

1164

            data_exists_symbol: ManuallyDrop::new(Symbol::new("Exists", 0)),

63

1164

            data_forall_symbol: ManuallyDrop::new(Symbol::new("Forall", 0)),

64

1164

            data_set_comprehension_symbol: ManuallyDrop::new(Symbol::new("SetComp", 0)),

65

1164

            data_bag_comprehension_symbol: ManuallyDrop::new(Symbol::new("BagComp", 0)),

66

1164

            data_untyped_set_bag_comprehension_symbol: ManuallyDrop::new(Symbol::new("UntypedSetBagComp", 0)),

67

1164

68

1164

            data_function_symbol: ManuallyDrop::new(Symbol::new("OpId", 2)),

69

1164

            data_function_symbol_no_index: ManuallyDrop::new(Symbol::new("OpIdNoIndex", 2)),

70

1164

            data_variable: ManuallyDrop::new(Symbol::new("DataVarId", 2)),

71

1164

            data_where_clause: ManuallyDrop::new(Symbol::new("Where", 2)),

72

1164

            data_untyped_identifier_clause: ManuallyDrop::new(Symbol::new("UntypedIdentifier", 1)),

73

1164

74

1164

            data_appl: Vec::new(),

75

1164

76

1164

77

78

    /// Returns true iff the given term is any of the possible data expressions.

79

    /// Note that this check is relatively expensive.

80

1597960973

    pub fn is_data_expression<'a, 'b, T: Term<'a, 'b>>(&mut self, term: &'b T) -> bool {

81

1597960973

        self.is_data_variable(term)

82

1595046570

            || self.is_data_function_symbol(term)

83

1414425943

            || self.is_data_machine_number(term)

84

1414421385

            || self.is_data_binder(term)

85

1414421385

            || self.is_data_where_clause(term)

86

1414421385

            || self.is_data_application(term)

87

1597960973

88

89

    /// Returns true iff the given term is a data variable.

90

1602630409

    pub fn is_data_variable<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

91

1602630409

        term.get_head_symbol() == self.data_variable.copy()

92

1602630409

93

94

    /// Returns true iff the given term is a data function symbol.

95

2483487901

    pub fn is_data_function_symbol<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

96

2483487901

        term.get_head_symbol() == self.data_function_symbol.copy()

97

1415891435

            || term.get_head_symbol() == self.data_function_symbol_no_index.copy()

98

2483487901

99

100

    /// Returns true iff the given term is a data machine number.

101

1414656355

    pub fn is_data_machine_number<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

102

1414656355

        is_int_term(term)

103

1414656355

104

105

    /// Returns true iff the given term is a data where clause.

106

1414421385

    pub fn is_data_where_clause<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

107

1414421385

        term.get_head_symbol() == self.data_where_clause.copy()

108

1414421385

109

110

    /// Returns true iff the given term is a data abstraction (binder).

111

1414421385

    pub fn is_data_binder<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

112

1414421385

        term.get_head_symbol() == self.data_binder_symbol.copy()

113

1414421385

114

115

    /// Returns true iff the given term is a data application.

116

2240170591

    pub fn is_data_application<'a, 'b, T: Term<'a, 'b>>(&mut self, term: &'b T) -> bool {

117

2240170591

        let arity = term.get_head_symbol().arity();

118

2240170591

        term.get_head_symbol() == *self.get_data_application_symbol(arity)

119

2240170591

120

121

    /// Returns the data application symbol for the given arity, creating it if necessary.

122

2330176829

    pub fn get_data_application_symbol(&mut self, arity: usize) -> &SymbolRef<'_> {

123

        // It can be that data_applications are created without create_data_application in the mcrl2 ffi.

124

2330176829

        if self.data_appl.len() <= arity {

125

1625

            self.data_appl.reserve(arity + 1 - self.data_appl.len());

126

5975

            while self.data_appl.len() <= arity {

127

4350

                let symbol = Symbol::new("DataAppl", self.data_appl.len());

128

4350

                self.data_appl.push(symbol);

129

4350

130

2330175204

131

132

2330176829

        self.data_appl[arity].get()

133

2330176829

134

135

    /// Returns true iff the given term is any sort expression (basic, arrow, container, structured,

136

    /// or untyped).

137

3

    pub fn is_sort_expression<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

138

3

        let sym = term.get_head_symbol();

139

3

        sym == self.basic_sort_symbol.copy()

140

            || sym == self.function_sort_symbol.copy()

141

            || sym == self.container_sort_symbol.copy()

142

            || sym == self.structured_sort_symbol.copy()

143

            || sym == self.untyped_sort_symbol.copy()

144

            || sym == self.untyped_possible_sorts_symbol.copy()

145

3

146

147

    /// Returns true iff the given term is a basic sort.

148

    pub fn is_basic_sort<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

149

        term.get_head_symbol() == self.basic_sort_symbol.copy()

150

151

152

153

// Helper functions to access the DATA_SYMBOLS thread local storage.

154

155

/// See [DataSymbols::is_sort_expression].

156

3

pub fn is_sort_expression<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

157

3

    DATA_SYMBOLS.with_borrow(|ds| ds.is_sort_expression(term))

158

3

159

160

/// See [DataSymbols::is_basic_sort].

161

pub fn is_basic_sort<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

162

    DATA_SYMBOLS.with_borrow(|ds| ds.is_basic_sort(term))

163

164

165

/// See [DataSymbols::is_data_variable].

166

4669436

pub fn is_data_variable<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

167

4669436

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_variable(term))

168

4669436

169

170

/// See [DataSymbols::is_data_expression].

171

1597960973

pub fn is_data_expression<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

172

1597960973

    DATA_SYMBOLS.with_borrow_mut(|ds| ds.is_data_expression(term))

173

1597960973

174

175

/// See [DataSymbols::is_data_function_symbol].

176

888441331

pub fn is_data_function_symbol<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

177

888441331

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_function_symbol(term))

178

888441331

179

180

/// See [DataSymbols::is_data_machine_number].

181

230412

pub fn is_data_machine_number<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

182

230412

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_machine_number(term))

183

230412

184

185

/// See [DataSymbols::is_data_where_clause].

186

pub fn is_data_where_clause<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

187

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_where_clause(term))

188

189

190

/// See [DataSymbols::is_data_binder].

191

pub fn is_data_binder<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

192

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_binder(term))

193

194

195

/// See [DataSymbols::is_data_application].

196

825749206

pub fn is_data_application<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

197

825749206

    DATA_SYMBOLS.with_borrow_mut(|ds| ds.is_data_application(term))

198

825749206