Skip to content

Commit

Permalink
Simplify handling of unreachable branches
Browse files Browse the repository at this point in the history 
Ref. #659
  • Loading branch information
@treiher
treiher committed Jun 8, 2021
1 parent 6d8a9a6 commit f2fda18
Show file tree
Hide file tree
Showing 24 changed files with 153 additions and 600 deletions.
15 changes: 15 additions & 0 deletions rflx/ada.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -719,6 +719,21 @@ def precedence(self) -> Precedence:
return Precedence.LITERAL


class Raise(Expr):
def __init__(self, identifier: StrID, string: Expr = None) -> None:
super().__init__()
self.identifier = ID(identifier)
self.string = string

def _update_str(self) -> None:
string = f" with {self.string}" if self.string else ""
self._str = intern(f"raise {self.identifier}{string}")

@property
def precedence(self) -> Precedence:
raise NotImplementedError


class Declaration(Base):
@abstractmethod
def __str__(self) -> str:
Expand Down
3 changes: 2 additions & 1 deletion rflx/generator/const.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,6 @@
TYPES_FIRST_BIT_INDEX = TYPES * "First_Bit_Index"
TYPES_LAST_BIT_INDEX = TYPES * "Last_Bit_Index"
TYPES_OFFSET = TYPES * "Offset"
TYPES_UNREACHABLE_BIT_LENGTH = TYPES * "Unreachable_Bit_Length"
TYPES_U64 = TYPES * "U64"

CONTEXT_INVARIANT = [
Expand All @@ -58,3 +57,5 @@
ada.Variable("Ctx.Last"),
)
]

UNREACHABLE = ada.Raise("Program_Error")
36 changes: 4 additions & 32 deletions rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1221,7 +1221,7 @@ def substituted(expression: expr.Expr) -> Expr:
else:
size = If(
[(substituted(l.condition), substituted(l.size)) for l in links],
Variable(const.TYPES_UNREACHABLE_BIT_LENGTH),
const.UNREACHABLE,
)
cases.append(
(
Expand All @@ -1234,7 +1234,7 @@ def substituted(expression: expr.Expr) -> Expr:
return Number(0)

if set(message.fields) - {l.target for l in message.outgoing(field)}:
cases.append((Variable("others"), Variable(const.TYPES_UNREACHABLE_BIT_LENGTH)))
cases.append((Variable("others"), const.UNREACHABLE))
return Case(Variable("Fld"), cases)

specification = FunctionSpecification(
Expand Down Expand Up @@ -1320,7 +1320,7 @@ def substituted(
)
for l in message.incoming(field)
],
Variable(const.TYPES_UNREACHABLE_BIT_LENGTH),
const.UNREACHABLE,
)

specification = FunctionSpecification(
Expand Down Expand Up @@ -2632,15 +2632,12 @@ def __create_type(self, field_type: Type, message_package: ID) -> None:

if isinstance(field_type, ModularInteger):
unit += UnitPart(modular_types(field_type))
unit += UnitPart(self.__type_dependent_unreachable_function(field_type))
unit += self.__integer_functions(field_type)
elif isinstance(field_type, RangeInteger):
unit += UnitPart(range_types(field_type))
unit += UnitPart(self.__type_dependent_unreachable_function(field_type))
unit += self.__integer_functions(field_type)
elif isinstance(field_type, Enumeration):
unit += UnitPart(enumeration_types(field_type))
unit += UnitPart(self.__type_dependent_unreachable_function(field_type))
unit += self.__enumeration_functions(field_type)
elif isinstance(field_type, Sequence):
self.__create_sequence_unit(field_type)
Expand Down Expand Up @@ -2822,9 +2819,7 @@ def __enumeration_functions(self, enum: Enumeration) -> UnitPart:
(value.ada_expr(), Variable(ID(key))) for key, value in enum.literals.items()
)
if incomplete:
conversion_cases.append(
(Variable("others"), Call(unreachable_function_name(enum.identifier)))
)
conversion_cases.append((Variable("others"), const.UNREACHABLE))

specification.extend(
[
Expand Down Expand Up @@ -3081,25 +3076,6 @@ def __type_validation_function(
validation_expression,
)

def __type_dependent_unreachable_function(self, scalar_type: Scalar) -> ty.List[Declaration]:
base_name = None
if isinstance(scalar_type, Enumeration) and scalar_type.always_valid:
base_name = self.__prefix * common.full_base_type_name(scalar_type)

type_name = self.__prefix * ID(scalar_type.identifier)

return [
Pragma("Warnings", [Variable("Off"), String("precondition is * false")]),
ExpressionFunctionDeclaration(
FunctionSpecification(unreachable_function_name(scalar_type.identifier), type_name),
First(type_name)
if not base_name
else Aggregate(Variable("False"), First(base_name)),
[Precondition(FALSE)],
),
Pragma("Warnings", [Variable("On"), String("precondition is * false")]),
]

def __integer_conversion_functions(self, integer: Integer) -> ty.Sequence[Subprogram]:
return [
ExpressionFunctionDeclaration(
Expand Down Expand Up @@ -3205,10 +3181,6 @@ def contains_function_name(refinement: Refinement) -> str:
return f"{sdu_name.flat}_In_{pdu_name.flat}_{refinement.field.name}"


def unreachable_function_name(type_identifier: expr.ID) -> str:
return f"Unreachable_{type_identifier.flat}"


def context_cursors_initialization(message: Message) -> Expr:
return NamedAggregate(
(
Expand Down
10 changes: 0 additions & 10 deletions rflx/templates/rflx_generic_types.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,14 +74,4 @@ is
Pre =>
(Offset'Pos (Off) + Value'Size - 1) / Byte'Size < Data'Length;

pragma Warnings (Off, "precondition is * false");

function Unreachable_Bit_Length return Bit_Length is
(Bit_Length'First)
with
Pre =>
False;

pragma Warnings (On, "precondition is * false");

end {prefix}RFLX_Generic_Types;
10 changes: 5 additions & 5 deletions tests/spark/generated/rflx-derivation-message.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -611,19 +611,19 @@ private
when F_Tag =>
RFLX.TLV.Tag_Base'Size,
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Tag =>
(case Fld is
when F_Length =>
RFLX.TLV.Length'Size,
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Length =>
(case Fld is
when F_Value =>
RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value.Length_Value) * 8,
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Value | F_Final =>
0));

Expand All @@ -638,14 +638,14 @@ private
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Value =>
(if
Ctx.Cursors (Fld).Predecessor = F_Length
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
RFLX_Types.Unreachable_Bit_Length)));
raise Program_Error)));

function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
(Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1);
Expand Down
10 changes: 0 additions & 10 deletions tests/spark/generated/rflx-enumeration.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,16 +22,6 @@ is
end case;
end record;

pragma Warnings (Off, "precondition is * false");

function Unreachable_Enumeration_Priority return RFLX.Enumeration.Priority is
((False, RFLX.Enumeration.Priority_Base'First))
with
Pre =>
False;

pragma Warnings (On, "precondition is * false");

pragma Warnings (Off, "unused variable ""Val""");

pragma Warnings (Off, "formal parameter ""Val"" is not referenced");
Expand Down
28 changes: 14 additions & 14 deletions tests/spark/generated/rflx-ethernet-frame.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -889,39 +889,39 @@ private
when F_Destination =>
RFLX.Ethernet.Address'Size,
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Destination =>
(case Fld is
when F_Source =>
RFLX.Ethernet.Address'Size,
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Source =>
(case Fld is
when F_Type_Length_TPID =>
RFLX.Ethernet.Type_Length_Base'Size,
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Type_Length_TPID =>
(case Fld is
when F_TPID =>
RFLX.Ethernet.TPID_Base'Size,
when F_Type_Length =>
RFLX.Ethernet.Type_Length_Base'Size,
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_TPID =>
(case Fld is
when F_TCI =>
RFLX.Ethernet.TCI'Size,
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_TCI =>
(case Fld is
when F_Type_Length =>
RFLX.Ethernet.Type_Length_Base'Size,
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Type_Length =>
(case Fld is
when F_Payload =>
Expand All @@ -934,9 +934,9 @@ private
then
RFLX_Types.Bit_Length (Ctx.Last) - RFLX_Types.Bit_Length (Ctx.Cursors (F_Type_Length).Last)
else
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when others =>
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Payload | F_Final =>
0));

Expand All @@ -950,29 +950,29 @@ private
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Type_Length_TPID =>
(if
Ctx.Cursors (Fld).Predecessor = F_Source
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_TPID =>
(if
Ctx.Cursors (Fld).Predecessor = F_Type_Length_TPID
and then Ctx.Cursors (F_Type_Length_TPID).Value.Type_Length_TPID_Value = 16#8100#
then
Ctx.Cursors (F_Type_Length_TPID).First
else
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_TCI =>
(if
Ctx.Cursors (Fld).Predecessor = F_TPID
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Type_Length =>
(if
Ctx.Cursors (Fld).Predecessor = F_TCI
Expand All @@ -984,7 +984,7 @@ private
then
Ctx.Cursors (F_Type_Length_TPID).First
else
RFLX_Types.Unreachable_Bit_Length),
raise Program_Error),
when F_Payload =>
(if
Ctx.Cursors (Fld).Predecessor = F_Type_Length
Expand All @@ -997,7 +997,7 @@ private
then
Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1
else
RFLX_Types.Unreachable_Bit_Length)));
raise Program_Error)));

function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
(Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1);
Expand Down
40 changes: 0 additions & 40 deletions tests/spark/generated/rflx-ethernet.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,16 +9,6 @@ is
Size =>
48;

pragma Warnings (Off, "precondition is * false");

function Unreachable_Ethernet_Address return RFLX.Ethernet.Address is
(RFLX.Ethernet.Address'First)
with
Pre =>
False;

pragma Warnings (On, "precondition is * false");

pragma Warnings (Off, "unused variable ""Val""");

pragma Warnings (Off, "formal parameter ""Val"" is not referenced");
Expand Down Expand Up @@ -47,16 +37,6 @@ is
Size =>
16;

pragma Warnings (Off, "precondition is * false");

function Unreachable_Ethernet_Type_Length return RFLX.Ethernet.Type_Length is
(RFLX.Ethernet.Type_Length'First)
with
Pre =>
False;

pragma Warnings (On, "precondition is * false");

function Valid (Val : RFLX.Ethernet.Type_Length_Base) return Boolean is
(Val >= 46);

Expand All @@ -77,16 +57,6 @@ is
Size =>
16;

pragma Warnings (Off, "precondition is * false");

function Unreachable_Ethernet_TPID return RFLX.Ethernet.TPID is
(RFLX.Ethernet.TPID'First)
with
Pre =>
False;

pragma Warnings (On, "precondition is * false");

function Valid (Val : RFLX.Ethernet.TPID_Base) return Boolean is
(Val = 16#8100#);

Expand All @@ -103,16 +73,6 @@ is
Size =>
16;

pragma Warnings (Off, "precondition is * false");

function Unreachable_Ethernet_TCI return RFLX.Ethernet.TCI is
(RFLX.Ethernet.TCI'First)
with
Pre =>
False;

pragma Warnings (On, "precondition is * false");

pragma Warnings (Off, "unused variable ""Val""");

pragma Warnings (Off, "formal parameter ""Val"" is not referenced");
Expand Down
Loading

0 comments on commit f2fda18

Please sign in to comment.