← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Structures/binarywrapper.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Structures/binarywrapper.h
1
 
/* VerifyPN - TAPAAL Petri Net Engine
2
 
 * Copyright (C) 2016  Peter Gjøl Jensen <root@petergjoel.dk>
3
 
 * 
4
 
 * This program is free software: you can redistribute it and/or modify
5
 
 * it under the terms of the GNU General Public License as published by
6
 
 * the Free Software Foundation, either version 3 of the License, or
7
 
 * (at your option) any later version.
8
 
 * 
9
 
 * This program is distributed in the hope that it will be useful,
10
 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11
 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12
 
 * GNU General Public License for more details.
13
 
 * 
14
 
 * You should have received a copy of the GNU General Public License
15
 
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
16
 
 */
17
 
 
18
 
/* 
19
 
 * File:   binarywrapper.h
20
 
 * Author: Peter G. Jensen
21
 
 *
22
 
 * Created on 10 June 2015, 19:20
23
 
 */
24
 
 
25
 
#include <iostream>
26
 
#include <string.h>
27
 
#include <assert.h>
28
 
#include <limits>
29
 
#include <stdlib.h>
30
 
#include <stdint.h>
31
 
 
32
 
#ifndef BINARYWRAPPER_H
33
 
#define BINARYWRAPPER_H
34
 
 
35
 
#define __BW_BSIZE__ sizeof(size_t) // SIZE OF POINTER!
36
 
namespace ptrie
37
 
{
38
 
    typedef unsigned int uint;
39
 
    typedef unsigned char uchar;
40
 
    
41
 
    /**
42
 
     * Wrapper for binary data. This provides easy access to individual bits, 
43
 
     * heap allocation and comparison. Notice that one has to make sure to 
44
 
     * explicitly call release() if one wishes to deallocate (possibly shared data).
45
 
     * 
46
 
     */
47
 
    class binarywrapper_t
48
 
    {
49
 
    public:
50
 
        // Constructors
51
 
        /**
52
 
         * Empty constructor, no data is allocated
53
 
         */
54
 
        
55
 
        binarywrapper_t() : _blob(NULL), _nbytes(0)
56
 
        {            
57
 
        }
58
 
        
59
 
        /**
60
 
         Allocates a room for at least size bits
61
 
         */
62
 
        
63
 
        binarywrapper_t(size_t size);
64
 
        
65
 
        /**
66
 
         * Constructor for copying over data from latest the offset'th bit.
67
 
         * Detects overflows.
68
 
         * @param other: wrapper to copy from
69
 
         * @param offset: maximal number of bits to skip.
70
 
         */
71
 
        
72
 
        binarywrapper_t(const binarywrapper_t& other, uint offset);
73
 
        
74
 
        inline void init(const binarywrapper_t& other, uint size, uint offset, 
75
 
                                                            uint encodingsize)
76
 
        {
77
 
            uint so = size + offset;
78
 
            offset = ((so - 1) / 8) - ((size - 1) / 8);
79
 
 
80
 
            _nbytes = ((encodingsize + this->overhead(encodingsize)) / 8);
81
 
            if (_nbytes > offset)
82
 
                _nbytes -= offset;
83
 
            else {
84
 
                _nbytes = 0;
85
 
            }
86
 
 
87
 
            _blob = allocate(_nbytes);
88
 
 
89
 
            memcpy(raw(), &(other.const_raw()[offset]), _nbytes);
90
 
        }
91
 
        
92
 
        
93
 
        binarywrapper_t(uchar* raw, uint size, uint offset, uint encsize);
94
 
        
95
 
        /**
96
 
         * Assign (not copy) raw data to pointer. Set number of bytes to size
97
 
         * @param raw: some memory to point to
98
 
         * @param size: number of bytes.
99
 
         */
100
 
        
101
 
        binarywrapper_t(uchar* raw, uint size);
102
 
        
103
 
        /**
104
 
         * Empty destructor. Does NOT deallocate data - do this with explicit
105
 
         * call to release().
106
 
         */
107
 
        
108
 
        ~binarywrapper_t()
109
 
        {        
110
 
        }
111
 
        
112
 
        /**
113
 
         * Makes a complete copy, including new heap-allocation
114
 
         * @return an exact copy, but in a different area of the heap.
115
 
         */
116
 
        
117
 
        //binarywrapper_t clone() const;
118
 
 
119
 
        /**
120
 
         * Copy over data and meta-data from other, but insert only into target
121
 
         * after offset bits.
122
 
         * Notice that this can cause memory-corruption if there is not enough
123
 
         * room in target, or to many bits are skipped.
124
 
         * @param other: wrapper to copy from
125
 
         * @param offset: bits to skip
126
 
         */
127
 
 
128
 
        void copy(const binarywrapper_t& other, uint offset);
129
 
 
130
 
        /**
131
 
         * Copy over size bytes form raw data. Assumes that current wrapper has
132
 
         * enough room.
133
 
         * @param raw: source data
134
 
         * @param size: number of bytes to copy
135
 
         */
136
 
 
137
 
        void copy(const uchar* raw, uint size);
138
 
 
139
 
        // accessors
140
 
        /**
141
 
         * Get value of the place'th bit
142
 
         * @param place: bit index
143
 
         * @return 
144
 
         */
145
 
        inline bool at(const uint place) const
146
 
        {
147
 
            uint offset = place % 8;
148
 
            bool res2;
149
 
            if (place / 8 < _nbytes)
150
 
                res2 = (const_raw()[place / 8] & _masks[offset]) != 0;
151
 
            else
152
 
                res2 = false;
153
 
 
154
 
            return res2;  
155
 
        } 
156
 
        
157
 
        /**
158
 
         * number of bytes allocated in heap
159
 
         * @return 
160
 
         */
161
 
        
162
 
        inline uint size() const
163
 
        {
164
 
            return _nbytes;
165
 
        }
166
 
                
167
 
        /**
168
 
         * Raw access to data when in const setting
169
 
         * @return 
170
 
         */
171
 
        
172
 
        inline uchar* const_raw() const
173
 
        {
174
 
            if(_nbytes <= __BW_BSIZE__) return offset((uchar*)&_blob, _nbytes);
175
 
            else 
176
 
                return offset(_blob, _nbytes);
177
 
        }
178
 
        
179
 
        /**
180
 
         * Raw access to data
181
 
         * @return 
182
 
         */
183
 
               
184
 
        inline uchar* raw()
185
 
        {
186
 
            return const_raw();
187
 
        }
188
 
 
189
 
        /**
190
 
         * pretty print of content
191
 
         */
192
 
        
193
 
        void print(std::ostream& strean, size_t length = std::numeric_limits<size_t>::max()) const;
194
 
        
195
 
        /**
196
 
         * finds the overhead (unused number of bits) when allocating for size
197
 
         * bits.
198
 
         * @param size: number of bits
199
 
         * @return 
200
 
         */
201
 
        
202
 
        static size_t overhead(size_t size);
203
 
        
204
 
        
205
 
        static size_t bytes(size_t size);
206
 
        // modifiers
207
 
        /**
208
 
         * Change value of place'th bit 
209
 
         * @param place: index of bit to change
210
 
         * @param value: desired value
211
 
         */
212
 
        
213
 
        inline void set(const uint place, const bool value) const
214
 
        {
215
 
            assert(place < _nbytes*8);
216
 
            uint offset = place % 8;
217
 
            uint theplace = place / 8;
218
 
            if (value) {
219
 
                const_raw()[theplace] |= _masks[offset];
220
 
            } else {
221
 
                const_raw()[theplace] &= ~_masks[offset];
222
 
            }    
223
 
        }   
224
 
        
225
 
        /**
226
 
         * Sets all memory on heap to 0 
227
 
         */
228
 
        
229
 
        inline void zero() const
230
 
        {
231
 
            if(_nbytes > 0 && _blob != NULL)
232
 
            {
233
 
                memset(const_raw(), 0x0, _nbytes); 
234
 
            }
235
 
        }
236
 
        
237
 
        /**
238
 
         * Deallocates memory stored on heap
239
 
         */
240
 
        
241
 
        inline void release()
242
 
        {
243
 
            if(_nbytes > __BW_BSIZE__)
244
 
                dealloc(_blob);
245
 
            _blob = NULL;
246
 
            _nbytes = 0;
247
 
        }
248
 
                
249
 
        /**
250
 
         * Nice access to single bits
251
 
         * @param i: index to access
252
 
         * @return 
253
 
         */
254
 
 
255
 
        inline uchar operator[](size_t i) const
256
 
        {
257
 
            if (i >= _nbytes) {
258
 
                 return 0x0;
259
 
            }
260
 
            return const_raw()[i]; 
261
 
        }
262
 
               
263
 
        
264
 
        /**
265
 
         * Compares two wrappers. Assumes that smaller number of bytes also means
266
 
         * a smaller wrapper. Otherwise compares byte by byte.
267
 
         * @param other: wrapper to compare to
268
 
         * @return -1 if other is smaller, 0 if same, 1 if other is larger
269
 
         */
270
 
        inline int cmp(const binarywrapper_t &other) const
271
 
        {
272
 
            if(_nbytes < other._nbytes) return -1;
273
 
            else if(_nbytes > other._nbytes) return 1;
274
 
            
275
 
            size_t bcmp = std::min(_nbytes, other._nbytes);
276
 
            return memcmp(const_raw(), other.const_raw(), bcmp);
277
 
        }
278
 
            
279
 
        /**
280
 
         * Compares wrappers bytes by bytes. If sizes do not match, they are not
281
 
         * equal. If sizes match, compares byte by byte.
282
 
         * @param enc1 
283
 
         * @param enc2
284
 
         * @return true if a match, false otherwise
285
 
         */
286
 
         friend bool operator==(  const binarywrapper_t &enc1, 
287
 
                                        const binarywrapper_t &enc2) {
288
 
            return enc1.cmp(enc2) == 0;
289
 
        }
290
 
         
291
 
        const static uchar _masks[8];
292
 
    private:
293
 
         
294
 
        static inline uchar* allocate(size_t n)
295
 
        {
296
 
            if(n <= __BW_BSIZE__) return 0;
297
 
#ifndef NDEBUG
298
 
            size_t on = n;
299
 
#endif            
300
 
            if(n % __BW_BSIZE__ != 0) n = (1+(n/__BW_BSIZE__))*(__BW_BSIZE__);
301
 
            assert(n % __BW_BSIZE__ == 0);
302
 
            assert(on <= n);
303
 
            return (uchar*)malloc(n);
304
 
        }
305
 
        
306
 
        static inline uchar* zallocate(size_t n)
307
 
        {
308
 
            if(n <= __BW_BSIZE__) return 0;
309
 
#ifndef NDEBUG
310
 
            size_t on = n;
311
 
#endif
312
 
            if(n % __BW_BSIZE__ != 0)
313
 
            {
314
 
                n = (1+(n/__BW_BSIZE__))*(__BW_BSIZE__);
315
 
                assert(n == on + (__BW_BSIZE__ - (on % __BW_BSIZE__)));
316
 
            }
317
 
            assert(n % __BW_BSIZE__ == 0);
318
 
            assert(on <= n);
319
 
            return (uchar*)calloc(n, 1);            
320
 
        }
321
 
        
322
 
        static inline void dealloc(uchar* data)
323
 
        {
324
 
            free(data);
325
 
        }
326
 
        
327
 
        static inline uchar* offset(uchar* data, uint32_t size)
328
 
        {
329
 
//            if((size % __BW_BSIZE__) == 0) return data;
330
 
//            else return &data[(__BW_BSIZE__ - (size % __BW_BSIZE__))];
331
 
            return data;
332
 
        }
333
 
        
334
 
        // blob of heap-allocated data
335
 
        uchar* _blob;
336
 
            
337
 
        // number of bytes allocated on heap
338
 
        uint32_t _nbytes;
339
 
               
340
 
        // masks for single-bit access
341
 
     } __attribute__((packed));
342
 
}
343
 
namespace std {
344
 
    std::ostream &operator<<(std::ostream &os, const ptrie::binarywrapper_t &b);
345
 
}
346
 
#endif  /* BINARYWRAPPER_H */
347