If one writes UINT32 t[:byte-size n], we actually generate a while-loop to validate each UINT32 advancing by 4 bytes each time. This is inefficient, since one could instead just check that n % 4 == 0 and skip over the array.
We already have an optimized combinator for integer types without refinements or actions, see
EverParse3d.Actions.Base.validate_nlist_constant_size_without_actions, but the interpreter does not seem to use it.
We should enhance the 3D interpreter to use the computed kinds and target this optimized combinator, i.e., relying on parser_kind_is_constant_size in TranslateForInterpreter.fst
If one writes
UINT32 t[:byte-size n]
, we actually generate a while-loop to validate each UINT32 advancing by 4 bytes each time. This is inefficient, since one could instead just check thatn % 4 == 0
and skip over the array.We already have an optimized combinator for integer types without refinements or actions, see EverParse3d.Actions.Base.validate_nlist_constant_size_without_actions, but the interpreter does not seem to use it.
We should enhance the 3D interpreter to use the computed kinds and target this optimized combinator, i.e., relying on parser_kind_is_constant_size in TranslateForInterpreter.fst