Currently, integer bounds checking ignores [requires], which means that $max_size_in_bytes and related values can be excessively large in some cases; e.g.:
struct Foo:
0 [+4] UInt size
[requires: this <= 16]
4 [+4] UInt message_type
8 [+size] UInt:8[] payload
# $max_size_in_bytes == 0xffff_ffff
# The real max size is 8 + 16 == 24.
The _compute_constraints_of_field_reference function in compiler/front_end/expression_bounds.py would need to be augmented to look for [requires] attributes and parse them for inferrable constraints (e.g., X && this <= 4, where X is any expression, puts an upper bound of 4 on the value). There is some similar expression analysis in write_inference.py, though the analysis there does not do what would be needed for bounds inference.
Currently, integer bounds checking ignores
[requires], which means that$max_size_in_bytesand related values can be excessively large in some cases; e.g.:The
_compute_constraints_of_field_referencefunction incompiler/front_end/expression_bounds.pywould need to be augmented to look for[requires]attributes and parse them for inferrable constraints (e.g.,X && this <= 4, whereXis any expression, puts an upper bound of4on the value). There is some similar expression analysis inwrite_inference.py, though the analysis there does not do what would be needed for bounds inference.