From f7387b3f45965c256cf49f6fc73e210e0f003df1 Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Tue, 2 Nov 2021 09:24:37 +0900 Subject: [PATCH] support variable buffer sizes in allocator Closes #713 --- rflx/generator/allocator.py | 107 ++++++--- rflx/generator/session.py | 5 +- rflx/model/__init__.py | 1 + rflx/model/session.py | 43 +++- rflx/specification/parser.py | 188 ++++++++++++++- .../generated/rflx-test-session_allocator.ads | 12 +- .../generated/rflx-test-session_allocator.ads | 12 +- .../generated/rflx-test-session_allocator.ads | 10 +- .../generated/rflx-test-session_allocator.ads | 10 +- .../generated/rflx-test-session_allocator.ads | 14 +- .../generated/rflx-test-session_allocator.ads | 16 +- .../generated/rflx-test-session_allocator.ads | 12 +- .../generated/rflx-test-session_allocator.ads | 12 +- .../generated/rflx-test-session_allocator.ads | 10 +- .../generated/rflx-test-session_allocator.ads | 10 +- .../generated/rflx-test-session_allocator.ads | 18 +- .../generated/rflx-test-session.ads | 2 +- .../generated/rflx-test-session_allocator.adb | 2 +- .../generated/rflx-test-session_allocator.ads | 10 +- tests/integration/session_simple/test.rfi | 6 + .../generated/rflx-test-session_allocator.ads | 10 +- tests/unit/specification/grammar_test.py | 4 +- tests/unit/specification/parser_test.py | 224 ++++++++++++++++++ 23 files changed, 614 insertions(+), 124 deletions(-) create mode 100644 tests/integration/session_simple/test.rfi diff --git a/rflx/generator/allocator.py b/rflx/generator/allocator.py index 77751546f6..532338eaa5 100644 --- a/rflx/generator/allocator.py +++ b/rflx/generator/allocator.py @@ -1,4 +1,5 @@ -from typing import Dict, List, Optional, Sequence, Set +from itertools import zip_longest +from typing import Dict, List, Optional, Sequence, Set, Tuple from rflx import expression as expr, typing_ as rty from rflx.ada import ( @@ -51,6 +52,7 @@ def __init__(self, session: Session, prefix: str = "") -> None: self._declaration_context: List[ContextItem] = [] self._body_context: List[ContextItem] = [] self._allocation_map: Dict[Location, int] = {} + self._size_map: Dict[int, int] = {} self._unit_part = UnitPart(specification=[Pragma("Elaborate_Body")]) self._all_slots: Set[int] = set() self._global_slots: Set[int] = set() @@ -95,32 +97,46 @@ def free_buffer(self, identifier: ID, location: Optional[Location]) -> Sequence[ ] @staticmethod - def _ptr_type() -> ID: - return ID("Slot_Ptr_Type") + def _ptr_type(size: int) -> ID: + return ID(f"Slot_Ptr_Type_{size}") def _create(self) -> None: - self._unit_part += self._create_ptr_subtype() + self._unit_part += self._create_ptr_subtypes() self._unit_part += self._create_slots() self._unit_part += self._create_init_pred() self._unit_part += self._create_init_proc() self._unit_part += self._create_global_allocated_pred() - def _create_ptr_subtype(self) -> UnitPart: - pred = OrElse( - Equal(Variable(self._ptr_type()), Variable("null")), - AndThen( - Equal(First(self._ptr_type()), First(const.TYPES_INDEX)), - Equal(Last(self._ptr_type()), Add(First(const.TYPES_INDEX), Number(4095))), - ), - ) - self._declaration_context.append(WithClause(self._prefix * const.TYPES_PACKAGE)) - self._declaration_context.append(UseTypeClause(self._prefix * const.TYPES_INDEX)) - self._declaration_context.append(UseTypeClause(self._prefix * const.TYPES_BYTES_PTR)) + def _create_ptr_subtypes(self) -> UnitPart: + sizes_set = set(self._size_map.values()) unit = UnitPart( specification=[ - Subtype(self._ptr_type(), const.TYPES_BYTES_PTR, aspects=[DynamicPredicate(pred)]), + Subtype( + self._ptr_type(cur_size), + const.TYPES_BYTES_PTR, + aspects=[ + DynamicPredicate( + OrElse( + Equal(Variable(self._ptr_type(cur_size)), Variable("null")), + AndThen( + Equal( + First(self._ptr_type(cur_size)), First(const.TYPES_INDEX) + ), + Equal( + Last(self._ptr_type(cur_size)), + Add(First(const.TYPES_INDEX), Number(cur_size - 1)), + ), + ), + ) + ) + ], + ) + for cur_size in sizes_set ] ) + self._declaration_context.append(WithClause(self._prefix * const.TYPES_PACKAGE)) + self._declaration_context.append(UseTypeClause(self._prefix * const.TYPES_INDEX)) + self._declaration_context.append(UseTypeClause(self._prefix * const.TYPES_BYTES_PTR)) return unit def _create_slots(self) -> UnitPart: @@ -132,7 +148,8 @@ def _create_slots(self) -> UnitPart: expression=NamedAggregate( ( ValueRange( - First(const.TYPES_INDEX), Add(First(const.TYPES_INDEX), Number(4095)) + First(const.TYPES_INDEX), + Add(First(const.TYPES_INDEX), Number(self._size_map[i] - 1)), ), First(const.TYPES_BYTE), ) @@ -144,7 +161,7 @@ def _create_slots(self) -> UnitPart: pointer_decls: List[Declaration] = [ ObjectDeclaration( [self._slot_id(i)], - self._ptr_type(), + self._ptr_type(self._size_map[i]), ) for i in self._all_slots ] @@ -218,27 +235,38 @@ def _needs_allocation(type_: rty.Type) -> bool: def _allocate_slots(self) -> None: """Create memory slots for each construct in the session that requires memory.""" + # pylint: disable=too-many-locals count: int = 0 - def insert(loc: Optional[Location]) -> None: + def create_slot_with_size(size: int) -> int: nonlocal count count += 1 - assert loc is not None - self._allocation_map[loc] = count self._all_slots.add(count) + self._size_map[count] = size + return count + + def map_sloc_to_slot(loc: Optional[Location], slot: int) -> None: + assert loc is not None + self._allocation_map[loc] = slot + # global variables for d in self._session.declarations.values(): if isinstance(d, decl.VariableDeclaration) and self._needs_allocation(d.type_): - insert(d.location) - self._global_slots.add(count) + slot = create_slot_with_size(self._session.buffer_sizes.get_size(d.identifier)) + map_sloc_to_slot(d.location, slot) + self._global_slots.add(slot) - global_count = count + # local variables + # get all allocation points and required sizes in a list (one element per state) + # of lists of tuples (loc, size) + + state_allocation_list = [] for s in self._session.states: - count = global_count + cur_state = [] for d in s.declarations.values(): if isinstance(d, decl.VariableDeclaration) and self._needs_allocation(d.type_): - insert(d.location) + cur_state.append((d.location, s.buffer_sizes.get_size(d.identifier))) for a in s.actions: if ( isinstance(a, stmt.Assignment) @@ -247,12 +275,33 @@ def insert(loc: Optional[Location]) -> None: and isinstance(a.expression.sequence.type_.element, rty.Message) and isinstance(a.expression.sequence, (expr.Selected, expr.Variable)) ): - insert(a.location) + cur_state.append((a.location, s.buffer_sizes.default_size)) if isinstance(a, stmt.Assignment) and isinstance(a.expression, expr.Head): - insert(a.location) + cur_state.append((a.location, s.buffer_sizes.default_size)) if ( isinstance(a, stmt.Write) and isinstance(a.parameter.type_, rty.Message) and not isinstance(a.parameter, expr.Variable) ): - insert(a.location) + cur_state.append((a.location, s.buffer_sizes.default_size)) + + state_allocation_list.append(cur_state) + # sort the list for each state by descending sizes + for entry in state_allocation_list: + entry.sort(key=lambda x: x[1], reverse=True) + + # get the list of max sizes for each slot + + def snd(arg: Tuple[Location, int]) -> int: + return arg[1] + + max_sizes_list = [ + max(map(snd, l)) for l in zip_longest(*state_allocation_list, fillvalue=(None, 0)) + ] + # create the actual slot with the max size for this element + states_slot_list = list(map(create_slot_with_size, max_sizes_list)) + # map the slocs to the corresponding memory slot + for entry in state_allocation_list: + assert len(entry) <= len(states_slot_list) + for ((sloc, _), slot) in zip(entry, states_slot_list): + map_sloc_to_slot(sloc, slot) diff --git a/rflx/generator/session.py b/rflx/generator/session.py index 48b14d8f53..7bef24412b 100644 --- a/rflx/generator/session.py +++ b/rflx/generator/session.py @@ -653,7 +653,10 @@ def _create_initialized_function(self, session: model.Session) -> UnitPart: ), Equal( # ISSUE: Componolit/RecordFlux#713 Variable(context_id(d.identifier) * "Buffer_Last"), - Add(First(const.TYPES_INDEX), Number(4095)), + Add( + First(const.TYPES_INDEX), + Number(session.buffer_sizes.get_size(d.identifier) - 1), + ), ), ] ], diff --git a/rflx/model/__init__.py b/rflx/model/__init__.py index 1ccf9473da..105cc70699 100644 --- a/rflx/model/__init__.py +++ b/rflx/model/__init__.py @@ -18,6 +18,7 @@ State as State, Transition as Transition, UnprovenSession as UnprovenSession, + defaultsizes as defaultsizes, ) from .type_ import ( # noqa: F401 BOOLEAN as BOOLEAN, diff --git a/rflx/model/session.py b/rflx/model/session.py index 77abbc095b..f31bad715f 100644 --- a/rflx/model/session.py +++ b/rflx/model/session.py @@ -1,6 +1,7 @@ import itertools from abc import abstractmethod from collections import defaultdict +from dataclasses import dataclass from typing import Dict, Iterable, List, Mapping, Optional, Sequence from rflx import expression as expr, typing_ as rty @@ -12,6 +13,19 @@ from . import BasicDeclaration, declaration as decl, statement as stmt, type_ as mty +@dataclass(order=True) +class BufferSizes: + default_size: int + size_map: Dict[str, int] + + def get_size(self, ident: ID) -> int: + name = ident.parts[-1] + return self.default_size if name not in self.size_map else self.size_map[name] + + +defaultsizes: BufferSizes = BufferSizes(default_size=4096, size_map={}) + + class Transition(Base): def __init__( self, @@ -36,7 +50,7 @@ def __str__(self) -> str: return f"goto {self.target}{with_aspects}{if_condition}" -class State(Base): +class State(Base): # pylint: disable=too-many-instance-attributes def __init__( self, identifier: StrID, @@ -45,6 +59,7 @@ def __init__( actions: Sequence[stmt.Statement] = None, declarations: Sequence[decl.BasicDeclaration] = None, description: str = None, + buffer_sizes: BufferSizes = defaultsizes, location: Location = None, ): # pylint: disable=too-many-arguments @@ -63,6 +78,7 @@ def __init__( self.declarations = {d.identifier: d for d in declarations} if declarations else {} self.description = description self.location = location + self.buffer_sizes = buffer_sizes def __repr__(self) -> str: return verbose_repr(self, ["identifier", "transitions", "actions", "declarations"]) @@ -142,6 +158,7 @@ def __init__( declarations: Sequence[decl.BasicDeclaration], parameters: Sequence[decl.FormalDeclaration], types: Sequence[mty.Type], + buffer_sizes: BufferSizes = defaultsizes, location: Location = None, ): super().__init__(identifier, location) @@ -152,6 +169,7 @@ def __init__( self.parameters = {p.identifier: p for p in parameters} self.types = {t.identifier: t for t in types} self.location = location + self.buffer_sizes = buffer_sizes refinements = [t for t in types if isinstance(t, Refinement)] @@ -244,10 +262,19 @@ def __init__( declarations: Sequence[decl.BasicDeclaration], parameters: Sequence[decl.FormalDeclaration], types: Sequence[mty.Type], + buffer_sizes: BufferSizes = defaultsizes, location: Location = None, ): super().__init__( - identifier, initial, final, states, declarations, parameters, types, location + identifier, + initial, + final, + states, + declarations, + parameters, + types, + buffer_sizes, + location, ) self.__validate() self.error.propagate() @@ -576,11 +603,20 @@ def __init__( declarations: Sequence[decl.BasicDeclaration], parameters: Sequence[decl.FormalDeclaration], types: Sequence[mty.Type], + buffer_sizes: BufferSizes = defaultsizes, location: Location = None, ): # pylint: disable=useless-super-delegation super().__init__( - identifier, initial, final, states, declarations, parameters, types, location + identifier, + initial, + final, + states, + declarations, + parameters, + types, + buffer_sizes, + location, ) def proven(self) -> Session: @@ -592,5 +628,6 @@ def proven(self) -> Session: list(self.declarations.values()), list(self.parameters.values()), list(self.types.values()), + self.buffer_sizes, self.location, ) diff --git a/rflx/specification/parser.py b/rflx/specification/parser.py index 9de17b5f91..b87a34b049 100644 --- a/rflx/specification/parser.py +++ b/rflx/specification/parser.py @@ -8,11 +8,13 @@ from typing import Callable, Dict, List, Mapping, Optional, Sequence, Set, Tuple, Type, Union import librflxlang as lang +from ruamel.yaml.main import YAML from rflx import expression as expr, model from rflx.error import Location, RecordFluxError, Severity, Subsystem, fail, warn from rflx.identifier import ID, StrID from rflx.model import declaration as decl, statement as stmt +from rflx.model.session import BufferSizes from rflx.specification.const import RESERVED_WORDS from . import style @@ -22,6 +24,97 @@ STDIN = Path("") +class InterfaceDescr: + @staticmethod + def _check_only_key( + filename: Path, + parent_key: Optional[str], + data: object, + unique_key: str, + ) -> object: + expl_str = "at toplevel" if parent_key is None else f'for key "{parent_key}"' + if not isinstance(data, dict): + fail( + f"{filename}: value {expl_str} is not a dictionary", + Subsystem.PARSER, + Severity.ERROR, + None, + ) + for key in data.keys(): + if key != unique_key: + fail( + f'{filename}: unexpected entry "{key}" in value {expl_str}', + Subsystem.PARSER, + Severity.ERROR, + None, + ) + if unique_key not in data: + fail( + f'{filename}: missing entry "{unique_key}" in value {expl_str}', + Subsystem.PARSER, + Severity.ERROR, + None, + ) + return data[unique_key] + + @staticmethod + def _check_is_size_entry(filename: Path, session: str, entry: Dict[str, object]) -> None: + for key, value in entry.items(): + if key == "Default": + if not isinstance(value, int): + fail( + ( + f"{filename}: value for default size " + f'for session "{session}" is not a number' + ), + Subsystem.PARSER, + Severity.ERROR, + None, + ) + else: + if not isinstance(value, dict): + fail( + f'{filename}: value for entry "{key}" is not a dictionary', + Subsystem.PARSER, + Severity.ERROR, + None, + ) + for k2, v2 in value.items(): + if not isinstance(v2, int): + fail( + f'{filename}: value for entry "{k2}" is not a number', + Subsystem.PARSER, + Severity.ERROR, + None, + ) + + def __init__(self, filename: Path) -> None: + self.filename = filename + self.session_map: Dict[str, object] = {} + yaml = YAML() + content = yaml.load(filename) + content = self._check_only_key(filename, None, content, "Session") + if not isinstance(content, dict): + fail( + f'{filename}: value for key "Session" is not a dictionary', + Subsystem.PARSER, + Severity.ERROR, + None, + ) + self.session_map = {} + for session, value in content.items(): + value = self._check_only_key(filename, session, value, "Buffer_Size") + if not isinstance(value, dict): + fail( + f'{filename}: value for key "Buffer_Size" is not a dictionary', + Subsystem.PARSER, + Severity.ERROR, + None, + ) + self._check_is_size_entry(filename, session, value) + self.session_map[session] = value + + def node_location(node: lang.RFLXNode, filename: Path, end_location: bool = False) -> Location: start = node.token_start.sloc_range end = node.token_end.sloc_range @@ -141,7 +234,10 @@ def create_statement(statement: lang.Statement, filename: Path) -> stmt.Statemen return handlers[statement.kind_name](statement, filename) -def create_state(state: lang.State, filename: Path) -> model.State: +def create_state( + state: lang.State, filename: Path, interface: Optional[InterfaceDescr] +) -> model.State: + # pylint: disable = too-many-locals location = node_location(state, filename) identifier = create_id(state.f_identifier, filename) if isinstance(state.f_body, lang.NullStateBody): @@ -171,6 +267,20 @@ def create_state(state: lang.State, filename: Path) -> model.State: for d in state.f_body.f_declarations: declarations.append(create_declaration(d, filename)) description = create_description(state.f_description) + if interface is not None: + for value in interface.session_map.values(): + assert isinstance(value, dict) + if state.f_identifier.text in value: + default_size = ( + value["Global"] if "Global" in value else model.defaultsizes.default_size + ) + state_sizes = BufferSizes( + default_size=default_size, size_map=dict(value[state.f_identifier.text]) + ) + else: + state_sizes = model.defaultsizes + else: + state_sizes = model.defaultsizes return model.State( identifier=identifier, transitions=transitions, @@ -178,6 +288,7 @@ def create_state(state: lang.State, filename: Path) -> model.State: actions=actions, declarations=declarations, description=description, + buffer_sizes=state_sizes, location=node_location(state, filename), ) @@ -198,16 +309,44 @@ def create_unproven_session( package: ID, filename: Path, types: Sequence[model.Type] = None, + interface: Optional[InterfaceDescr] = None, ) -> model.UnprovenSession: __check_session_identifier(session, filename) + + if interface is not None: + session_info = interface.session_map[session.f_identifier.text] + assert isinstance(session_info, dict) + if "Global" in session_info: + for key in session_info["Global"].keys(): + if key not in [ + x.f_identifier.text + for x in session.f_declarations + if isinstance(x, lang.VariableDecl) + ]: + fail( + ( + f'{interface.filename}: unknown variable "{key}" in ' + f'global state of session "{session.f_identifier.text}"' + ), + Subsystem.PARSER, + Severity.ERROR, + ) + global_sizes = BufferSizes( + default_size=session_info["Default"] if "Default" in session_info else 4096, + size_map=dict(session_info["Global"]) if "Global" in session_info else {}, + ) + + else: + global_sizes = model.defaultsizes return model.UnprovenSession( package * create_id(session.f_identifier, filename), create_id(session.f_aspects.f_initial, filename), create_id(session.f_aspects.f_final, filename), - [create_state(s, filename) for s in session.f_states], + [create_state(s, filename, interface) for s in session.f_states], [create_declaration(d, filename) for d in session.f_declarations], [create_formal_declaration(p, filename) for p in session.f_parameters], types or [], + global_sizes, node_location(session, filename), ) @@ -217,8 +356,9 @@ def create_session( package: ID, filename: Path, types: Sequence[model.Type] = None, + interface: Optional[InterfaceDescr] = None, ) -> model.Session: - return create_unproven_session(session, package, filename, types).proven() + return create_unproven_session(session, package, filename, types, interface).proven() def create_id(identifier: lang.AbstractID, filename: Path) -> ID: @@ -1416,6 +1556,7 @@ class SpecificationNode: filename: Path spec: lang.Specification withed_files: List[str] + interface: Optional[InterfaceDescr] class Parser: @@ -1440,6 +1581,7 @@ def __convert_unit( spec: lang.Specification, filename: Path, transitions: List[ID] = None, + interface: InterfaceDescr = None, ) -> None: transitions = transitions or [] withed_files = [] @@ -1499,7 +1641,9 @@ def __convert_unit( ), ], ) - self.__specifications[packagefile] = SpecificationNode(filename, spec, withed_files) + self.__specifications[packagefile] = SpecificationNode( + filename, spec, withed_files, interface + ) def __parse_specfile(self, filename: Path, transitions: List[ID] = None) -> RecordFluxError: error = RecordFluxError() @@ -1509,9 +1653,13 @@ def __parse_specfile(self, filename: Path, transitions: List[ID] = None) -> Reco unit = lang.AnalysisContext().get_from_file(str(filename)) if diagnostics_to_error(unit.diagnostics, error, filename): return error + interface_file = filename.with_suffix(".rfi") + interface = None + if interface_file.exists(): + interface = InterfaceDescr(interface_file) if unit.root: assert isinstance(unit.root, lang.Specification) - self.__convert_unit(error, unit.root, filename, transitions) + self.__convert_unit(error, unit.root, filename, transitions, interface) return error def __sort_specs_topologically(self) -> None: @@ -1543,6 +1691,22 @@ def parse(self, *specfiles: Path) -> None: for f in specfiles: error.extend(self.__parse_specfile(f)) error.extend(style.check(f)) + for spec_node in self.__specifications.values(): + if spec_node.interface is not None: + for rfi_session in spec_node.interface.session_map.keys(): + session_ids = [ + x.f_identifier.text + for x in spec_node.spec.f_package_declaration.f_declarations + if isinstance(x, lang.SessionDecl) + ] + print(session_ids) + if rfi_session not in session_ids: + fail( + f'{spec_node.interface.filename}: unknown session "{rfi_session}"', + Subsystem.PARSER, + Severity.ERROR, + None, + ) self.__sort_specs_topologically() error.propagate() @@ -1555,14 +1719,16 @@ def parse_string( unit = lang.AnalysisContext().get_from_buffer("", string, rule=rule) if not diagnostics_to_error(unit.diagnostics, error, STDIN): assert isinstance(unit.root, lang.Specification) - self.__convert_unit(error, unit.root, STDIN) + self.__convert_unit(error, unit.root, STDIN, interface=None) self.__sort_specs_topologically() error.propagate() def create_model(self) -> model.Model: error = RecordFluxError() for spec_node in self.__specifications.values(): - self.__evaluate_specification(error, spec_node.spec, spec_node.filename) + self.__evaluate_specification( + error, spec_node.spec, spec_node.filename, spec_node.interface + ) try: result = model.Model(self.__types, self.__sessions) except RecordFluxError as e: @@ -1579,7 +1745,11 @@ def specifications(self) -> Dict[str, lang.Specification]: } def __evaluate_specification( - self, error: RecordFluxError, spec: lang.Specification, filename: Path + self, + error: RecordFluxError, + spec: lang.Specification, + filename: Path, + interface: Optional[InterfaceDescr], ) -> None: handlers: Dict[ str, @@ -1639,7 +1809,7 @@ def __evaluate_specification( error.extend(e) elif isinstance(t, lang.SessionDecl): try: - new_session = create_session(t, package_id, filename, self.__types) + new_session = create_session(t, package_id, filename, self.__types, interface) self.__sessions.append(new_session) error.extend(new_session.error) except RecordFluxError as e: diff --git a/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.ads b/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.ads index 44a59973f8..bd9245ecf0 100644 --- a/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.ads +++ b/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.ads @@ -12,15 +12,15 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; - Slot_Ptr_2 : Slot_Ptr_Type; + Slot_Ptr_2 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null diff --git a/tests/integration/session_append_unconstrained/generated/rflx-test-session_allocator.ads b/tests/integration/session_append_unconstrained/generated/rflx-test-session_allocator.ads index 44a59973f8..bd9245ecf0 100644 --- a/tests/integration/session_append_unconstrained/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_append_unconstrained/generated/rflx-test-session_allocator.ads @@ -12,15 +12,15 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; - Slot_Ptr_2 : Slot_Ptr_Type; + Slot_Ptr_2 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null diff --git a/tests/integration/session_binding/generated/rflx-test-session_allocator.ads b/tests/integration/session_binding/generated/rflx-test-session_allocator.ads index 58a24297c4..17e830e759 100644 --- a/tests/integration/session_binding/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_binding/generated/rflx-test-session_allocator.ads @@ -12,13 +12,13 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null); diff --git a/tests/integration/session_channels/generated/rflx-test-session_allocator.ads b/tests/integration/session_channels/generated/rflx-test-session_allocator.ads index 58a24297c4..17e830e759 100644 --- a/tests/integration/session_channels/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_channels/generated/rflx-test-session_allocator.ads @@ -12,13 +12,13 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null); diff --git a/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session_allocator.ads b/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session_allocator.ads index 46311f5bf4..556679e5d1 100644 --- a/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_comprehension_on_message_field/generated/rflx-test-session_allocator.ads @@ -12,17 +12,17 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; - Slot_Ptr_2 : Slot_Ptr_Type; + Slot_Ptr_2 : Slot_Ptr_Type_4096; - Slot_Ptr_3 : Slot_Ptr_Type; + Slot_Ptr_3 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session_allocator.ads b/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session_allocator.ads index d563c2814f..31bca7b9d5 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session_allocator.ads @@ -12,19 +12,19 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; - Slot_Ptr_2 : Slot_Ptr_Type; + Slot_Ptr_2 : Slot_Ptr_Type_4096; - Slot_Ptr_3 : Slot_Ptr_Type; + Slot_Ptr_3 : Slot_Ptr_Type_4096; - Slot_Ptr_4 : Slot_Ptr_Type; + Slot_Ptr_4 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null diff --git a/tests/integration/session_conversion/generated/rflx-test-session_allocator.ads b/tests/integration/session_conversion/generated/rflx-test-session_allocator.ads index 44a59973f8..bd9245ecf0 100644 --- a/tests/integration/session_conversion/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_conversion/generated/rflx-test-session_allocator.ads @@ -12,15 +12,15 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; - Slot_Ptr_2 : Slot_Ptr_Type; + Slot_Ptr_2 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null diff --git a/tests/integration/session_functions/generated/rflx-test-session_allocator.ads b/tests/integration/session_functions/generated/rflx-test-session_allocator.ads index 44a59973f8..bd9245ecf0 100644 --- a/tests/integration/session_functions/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_functions/generated/rflx-test-session_allocator.ads @@ -12,15 +12,15 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; - Slot_Ptr_2 : Slot_Ptr_Type; + Slot_Ptr_2 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null diff --git a/tests/integration/session_minimal/generated/rflx-test-session_allocator.ads b/tests/integration/session_minimal/generated/rflx-test-session_allocator.ads index 58a24297c4..17e830e759 100644 --- a/tests/integration/session_minimal/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_minimal/generated/rflx-test-session_allocator.ads @@ -12,13 +12,13 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null); diff --git a/tests/integration/session_reuse_of_message/generated/rflx-test-session_allocator.ads b/tests/integration/session_reuse_of_message/generated/rflx-test-session_allocator.ads index 58a24297c4..17e830e759 100644 --- a/tests/integration/session_reuse_of_message/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_reuse_of_message/generated/rflx-test-session_allocator.ads @@ -12,13 +12,13 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null); diff --git a/tests/integration/session_sequence_append_head/generated/rflx-test-session_allocator.ads b/tests/integration/session_sequence_append_head/generated/rflx-test-session_allocator.ads index b2c4045536..8426ff7edb 100644 --- a/tests/integration/session_sequence_append_head/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_sequence_append_head/generated/rflx-test-session_allocator.ads @@ -12,21 +12,21 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; - Slot_Ptr_2 : Slot_Ptr_Type; + Slot_Ptr_2 : Slot_Ptr_Type_4096; - Slot_Ptr_3 : Slot_Ptr_Type; + Slot_Ptr_3 : Slot_Ptr_Type_4096; - Slot_Ptr_4 : Slot_Ptr_Type; + Slot_Ptr_4 : Slot_Ptr_Type_4096; - Slot_Ptr_5 : Slot_Ptr_Type; + Slot_Ptr_5 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null diff --git a/tests/integration/session_simple/generated/rflx-test-session.ads b/tests/integration/session_simple/generated/rflx-test-session.ads index 8d849b8097..45ee35e50c 100644 --- a/tests/integration/session_simple/generated/rflx-test-session.ads +++ b/tests/integration/session_simple/generated/rflx-test-session.ads @@ -75,7 +75,7 @@ private function Initialized return Boolean is (Universal.Message.Has_Buffer (Message_Ctx) and then Message_Ctx.Buffer_First = RFLX_Types.Index'First - and then Message_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095 + and then Message_Ctx.Buffer_Last = RFLX_Types.Index'First + 1023 and then Test.Session_Allocator.Global_Allocated); function Active return Boolean is diff --git a/tests/integration/session_simple/generated/rflx-test-session_allocator.adb b/tests/integration/session_simple/generated/rflx-test-session_allocator.adb index a55f641bf8..89d53db69c 100644 --- a/tests/integration/session_simple/generated/rflx-test-session_allocator.adb +++ b/tests/integration/session_simple/generated/rflx-test-session_allocator.adb @@ -5,7 +5,7 @@ package body RFLX.Test.Session_Allocator with SPARK_Mode is - Slot_1 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First); + Slot_1 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 1023 => RFLX_Types.Byte'First); procedure Initialize with SPARK_Mode => diff --git a/tests/integration/session_simple/generated/rflx-test-session_allocator.ads b/tests/integration/session_simple/generated/rflx-test-session_allocator.ads index 58a24297c4..2b3696d17c 100644 --- a/tests/integration/session_simple/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_simple/generated/rflx-test-session_allocator.ads @@ -12,13 +12,13 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_1024 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_1024 = null + or else (Slot_Ptr_Type_1024'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_1024'Last = RFLX_Types.Index'First + 1023); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_1024; function Initialized return Boolean is (Slot_Ptr_1 /= null); diff --git a/tests/integration/session_simple/test.rfi b/tests/integration/session_simple/test.rfi new file mode 100644 index 0000000000..5b5be9bb4b --- /dev/null +++ b/tests/integration/session_simple/test.rfi @@ -0,0 +1,6 @@ +Session: + Session: + Buffer_Size: + Default: 2048 + Global: + Message: 1024 diff --git a/tests/integration/session_variable_initialization/generated/rflx-test-session_allocator.ads b/tests/integration/session_variable_initialization/generated/rflx-test-session_allocator.ads index a241f1ee78..2eb4036e64 100644 --- a/tests/integration/session_variable_initialization/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_variable_initialization/generated/rflx-test-session_allocator.ads @@ -12,13 +12,13 @@ is pragma Elaborate_Body; - subtype Slot_Ptr_Type is RFLX_Types.Bytes_Ptr with + subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with Dynamic_Predicate => - Slot_Ptr_Type = null - or else (Slot_Ptr_Type'First = RFLX_Types.Index'First - and then Slot_Ptr_Type'Last = RFLX_Types.Index'First + 4095); + Slot_Ptr_Type_4096 = null + or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First + and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095); - Slot_Ptr_1 : Slot_Ptr_Type; + Slot_Ptr_1 : Slot_Ptr_Type_4096; function Initialized return Boolean is (Slot_Ptr_1 /= null); diff --git a/tests/unit/specification/grammar_test.py b/tests/unit/specification/grammar_test.py index c16b9b5475..aa3040b436 100644 --- a/tests/unit/specification/grammar_test.py +++ b/tests/unit/specification/grammar_test.py @@ -49,7 +49,7 @@ def parse_formal_declaration(data: str) -> decl.Declaration: def parse_state(data: str) -> State: parser_state, source = parse(data, lang.GrammarRule.state_rule) assert isinstance(parser_state, lang.State) - state = create_state(parser_state, source) + state = create_state(parser_state, source, interface=None) assert isinstance(state, State) return state @@ -866,7 +866,7 @@ def test_state_error(string: str, error: str) -> None: decl.FunctionDeclaration("F", [], "T"), ], [], - Location((2, 16), None, (23, 27)), + location=Location((2, 16), None, (23, 27)), ), ), ], diff --git a/tests/unit/specification/parser_test.py b/tests/unit/specification/parser_test.py index ded56ae054..e776e17690 100644 --- a/tests/unit/specification/parser_test.py +++ b/tests/unit/specification/parser_test.py @@ -2802,3 +2802,227 @@ def test_parse_reserved_word_as_channel_name() -> None: end Test; """ ) + + +@pytest.mark.parametrize( + "raises, rfi_content,match_error", + [ + (True, "garbage", "test.rfi: value at toplevel is not a dictionary"), + (True, "Other: some entry", 'test.rfi: unexpected entry "Other" in value at toplevel'), + (True, "Session: garbage", 'test.rfi: value for key "Session" is not a dictionary'), + (True, "{}", 'test.rfi: missing entry "Session" in value at toplevel'), + ( + True, + """Session: + Session: 1 + """, + 'test.rfi: value for key "Session" is not a dictionary', + ), + ( + True, + """Session: + No_Session: + Buffer_Size: + Default: 1024 + Global: + Message: 2048 + """, + 'test.rfi: unknown session "No_Session"', + ), + ( + True, + """Session: + Session: + Garbage: 1 + """, + 'test.rfi: unexpected entry "Garbage" in value for key "Session"', + ), + ( + True, + """Session: + Session: + Buffer_Size: + Random: 1 + """, + 'test.rfi: value for entry "Random" is not a dictionary', + ), + ( + True, + """Session: + Session: + Buffer_Size: + Default: 1024 + Global: + Message: 2048 + """, + 'test.rfi: unknown variable "Message" in global state of session "Session"', + ), + ( + True, + """Session: + Session: + Buffer_Size: + Default: Hello + Global: + Msg: 2048 + """, + 'test.rfi: value for default size for session "Session" is not a number', + ), + ( + True, + """Session: + Session: + Buffer_Size: + Default: 1024 + Global: + Msg: Hello + """, + 'test.rfi: value for entry "Msg" is not a number', + ), + ( + True, + """Session: + Session: + Buffer_Size: 2 + """, + 'test.rfi: value for key "Buffer_Size" is not a dictionary', + ), + ( + False, + """Session: + Session: + Buffer_Size: + Default: 1024 + Global: + Msg: 2048 + Start: {} + """, + "", + ), + ( + False, + """Session: + Session: + Buffer_Size: + Default: 1024 + Start: {} + """, + "", + ), + ], +) +def test_rfi_files(raises: bool, tmp_path: Path, rfi_content: str, match_error: str) -> None: + p = parser.Parser() + content = """package Test is + type Message_Type is (MT_Null => 0, MT_Data => 1, MT_Value => 2, MT_Values => 3, MT_Option_Types => 4, + MT_Options => 5, MT_Unconstrained_Data => 6, MT_Unconstrained_Options => 7) with Size => 8; + + type Length is range 0 .. 2 ** 16 - 1 with Size => 16; + + type ValueT is mod 256; + + type Values is sequence of ValueT; + + type Option_Type is (OT_Null => 0, OT_Data => 1) with Size => 8, Always_Valid => True; + + type Option_Types is sequence of Option_Type; + + type Option is + message + Option_Type : Option_Type + then null + if Option_Type = OT_Null + then Length + if Option_Type = OT_Data; + Length : Length + then Data + with Size => Length * 8; + Data : Opaque; + end message; + type Options is sequence of Option; + type Message is + message + Message_Type : Message_Type + then null + if Message_Type = MT_Null + then Data + with Size => Message'Last - Message_Type'Last + if Message_Type = MT_Unconstrained_Data + then Length + if Message_Type /= MT_Null + and Message_Type /= MT_Unconstrained_Data + and Message_Type /= MT_Unconstrained_Options + then Options + with Size => Message'Last - Message_Type'Last + if Message_Type = MT_Unconstrained_Options; + Length : Length + then Data + with Size => Length * 8 + if Message_Type = MT_Data + then Option_Types + with Size => Length * 8 + if Message_Type = MT_Option_Types + then Options + with Size => Length * 8 + if Message_Type = MT_Options + then Value + if Message_Type = MT_Value + and Length = 1 + then Values + with Size => Length * 8 + if Message_Type = MT_Values; + Data : Opaque + then null; + Option_Types : Option_Types + then null; + Options : Options + then null; + Value : ValueT + then null; + Values : Values; + end message; + + for Message use (Data => Option); + + generic + Channel : Channel with Readable, Writable; + session Session with + Initial => Start, + Final => Terminated + is + Msg : Message; + begin + state Start is + begin + Channel'Read (Msg); + transition + goto Reply + if Msg'Valid = True + and Msg.Message_Type = MT_Data + and Msg.Length = 1 + goto Terminated + end Start; + state Reply is + begin + MSg := Message'(Message_Type => MT_Data, Length => 1, Data => [2]); + Channel'Write (Msg); + transition + goto Terminated + exception + goto Terminated + end Reply; + state Terminated is null state; + end Session; + end Test; +""" + test_spec = tmp_path / "test.rflx" + test_rfi = tmp_path / "test.rfi" + test_spec.write_text(content, encoding="utf-8") + test_rfi.write_text(rfi_content) + if raises: + with pytest.raises(RecordFluxError, match=match_error): + p.parse(test_spec) + p.create_model() + else: + p.parse(test_spec) + p.create_model()