seL4/tools/bitfield_gen.py

42 # Isabelle word size suffixes for return value names
1184 def field_mask_proof(base, base_bits, sign_extend, high, size):
1188             return "NOT (mask %d)" % (base_bits - size)
1190             return "(mask %d << %d)" % (size, base_bits - size)
1192         return "mask %d" % size
1225         # Ensure that block sizes and tag size & position match for
1239                 union_size = ref.size
1240             elif union_size != ref.size:
1383                     offset, size, high = ref.field_map[field]
1388                     mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size)
1411             _, size, _ = ref.field_map[self.tagname]
1412             if any([w for w in self.widths if w < size]):
1419             for (field, offset, size, high) in ref.fields:
1423                 mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size)
1574             offset, size, _ = ref.field_map[self.tagname]
1575             part_widths = [w for w in self.widths if w < size]
1579                         "full_mask":    hex(2 ** size - 1),
1599                 offset, size, high = ref.field_map[field]
1608                     shift = self.base_bits - size - (offset % self.base)
1623                 if size < self.base:
1624                     mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size)
1775                 offset, size, high = ref.field_map[field]
1785                     shift = self.base_bits - size - (offset % self.base)
1797                 if size < self.base:
1799                         mask = ((1 << size) - 1) << (self.base_bits - size)
1801                         mask = (1 << size) - 1
1842             for field, offset, size, high in ref.fields:
1850                     shift = self.base_bits - size - (offset % self.base)
1864                 mask = ((1 << size) - 1) << (offset % self.base)
2032             offset, size, _ = ref.field_map[self.tagname]
2033             used.add(size)
2034             self.tag_offset[size] = offset
2107         self.size = sum(size for _name, size, _high in fields)
2108         offset = self.size
2124         self.field_map = dict((name, (offset, size, high)) \
2125                               for name, offset, size, high in _fields)
2147         if self.size % base != 0:
2150         self.multiple = self.size // base
2151         for name, offset, size, high in self.fields:
2152             if offset // base != (offset+size-1) // base:
2189                 offset, size, high = self.field_map[name]
2196                     shift = self.base_bits - size - (offset % self.base)
2211                 if size < self.base:
2212                     mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size)
2261                     (field, offset, size, high) in self.fields]
2274         for (field, offset, size, high) in self.fields:
2275             mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size)
2297         for (field, offset, size, high) in self.fields:
2298             mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size)
2391         for field, offset, size, high in self.fields:
2395                 shift = self.base_bits - size - (offset % self.base)
2407             if size < self.base:
2409                     mask = ((1 << size) - 1) << (self.base_bits - size)
2411                     mask = (1 << size) - 1
2449         for field, offset, size, high in self.fields:
2454                 shift = self.base_bits - size - (offset % self.base)
2468             mask = ((1 << size) - 1) << (offset % self.base)
2537         for field, offset, size, high in self.fields:
2654                 raise ValueError("Invalid base size: %d" % base)
2668                 raise ValueError("Invalid base size: %d" % base)