Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

disable inlining via trivial postconditions #938

Merged
merged 1 commit into from
Feb 17, 2022
Merged

disable inlining via trivial postconditions #938

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
105 changes: 85 additions & 20 deletions rflx/generator/generator.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -525,6 +525,11 @@ def __create_cursor_type(message: Message) -> UnitPart:
PrivateType("Field_Cursors", aspects=[DefaultInitialCondition(FALSE)]),
],
private=[
# WORKAROUND: Componolit/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
ExpressionFunctionDeclaration(
FunctionSpecification(
"Valid_Value", "Boolean", [Parameter(["Val"], "Field_Dependent_Value")]
Expand All @@ -545,6 +550,11 @@ def __create_cursor_type(message: Message) -> UnitPart:
(Variable(FINAL.affixed_name), FALSE),
],
),
[Postcondition(TRUE)],
),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
RecordType(
"Field_Cursor",
Expand Down Expand Up @@ -1039,7 +1049,18 @@ def __create_initialized_function(message: Message) -> UnitPart:
first_field = message.fields[0]

return UnitPart(
[SubprogramDeclaration(specification, [Ghost()])],
[
# WORKAROUND: Componolit/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
SubprogramDeclaration(specification, [Ghost(), Postcondition(TRUE)]),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
],
private=[
ExpressionFunctionDeclaration(
specification,
Expand Down Expand Up @@ -1673,16 +1694,26 @@ def condition(field: Field, message: Message) -> Expr:

return UnitPart(
[
# WORKAROUND Compolonit/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
SubprogramDeclaration(
specification,
[
Precondition(
And(
Call("Valid_Predecessor", [Variable("Ctx"), Variable("Fld")]),
)
)
),
Postcondition(TRUE),
],
)
),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
],
private=[
ExpressionFunctionDeclaration(
Expand Down Expand Up @@ -1875,16 +1906,26 @@ def substituted(

return UnitPart(
[
# WORKAROUND Compolonit/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
SubprogramDeclaration(
specification,
[
Precondition(
And(
Call("Valid_Next", [Variable("Ctx"), Variable("Fld")]),
)
)
),
Postcondition(TRUE),
],
)
),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
],
private=[
ExpressionFunctionDeclaration(
Expand Down Expand Up @@ -2021,6 +2062,11 @@ def condition(field: Field, message: Message) -> Expr:

return UnitPart(
[
# WORKAROUND Compolonit/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
SubprogramDeclaration(
specification,
[
Expand All @@ -2030,9 +2076,14 @@ def condition(field: Field, message: Message) -> Expr:
In(Variable("Val.Fld"), Range("Field")),
Call("Valid_Predecessor", [Variable("Ctx"), Variable("Val.Fld")]),
)
)
),
Postcondition(TRUE),
],
)
),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
],
private=[
ExpressionFunctionDeclaration(
Expand All @@ -2057,7 +2108,18 @@ def __create_predecessor_function() -> UnitPart:
)

return UnitPart(
[SubprogramDeclaration(specification)],
[
# WORKAROUND Compolonit/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
SubprogramDeclaration(specification, [Postcondition(TRUE)]),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
],
private=[
ExpressionFunctionDeclaration(
specification,
Expand Down Expand Up @@ -2399,7 +2461,18 @@ def __create_valid_predecessor_function(
)

return UnitPart(
[SubprogramDeclaration(specification)],
[
# WORKAROUND Compolonit/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
SubprogramDeclaration(specification, [Postcondition(TRUE)]),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
],
private=[
ExpressionFunctionDeclaration(
specification,
Expand Down Expand Up @@ -3254,15 +3327,10 @@ def __create_valid_context_function(
String('"Buffer" is not modified, could be of access constant type'),
],
),
# We want to avoid inlining of the context predicate for proof. The way to do
# that in SPARK Pro 23.x is to add a dummy postcondition ("True"). We silence
# the warning that this dummy postcondition doesn't mention the function result.
# WORKAROUND: Componolit/Workarounds#47
Pragma(
"Warnings",
[
Variable("Off"),
String("postcondition does not mention function result"),
],
[Variable("Off"), String("postcondition does not mention function result")],
),
ExpressionFunctionDeclaration(
specification,
Expand All @@ -3278,10 +3346,7 @@ def __create_valid_context_function(
),
Pragma(
"Warnings",
[
Variable("On"),
String("postcondition does not mention function result"),
],
[Variable("On"), String("postcondition does not mention function result")],
),
],
)
Expand Down
13 changes: 12 additions & 1 deletion rflx/generator/parser.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -678,7 +678,18 @@ def create_incomplete_message_function(message: Message) -> UnitPart:
)

return UnitPart(
[SubprogramDeclaration(specification)],
[
# WORKAROUND Compolonit/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
SubprogramDeclaration(specification, [Postcondition(TRUE)]),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
],
private=[
ExpressionFunctionDeclaration(
specification,
Expand Down
15 changes: 13 additions & 2 deletions rflx/generator/serializer.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@
OutParameter,
Parameter,
Postcondition,
Pragma,
PragmaStatement,
Precondition,
ProcedureSpecification,
Expand Down Expand Up @@ -326,16 +327,26 @@ def substituted(expression: expr.Expr) -> Expr:

return UnitPart(
[
# WORKAROUND Compolonit/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
SubprogramDeclaration(
specification,
[
Precondition(
And(
Call("Valid_Next", [Variable("Ctx"), Variable("Fld")]),
)
)
),
Postcondition(TRUE),
],
)
),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
],
private=[
ExpressionFunctionDeclaration(
Expand Down
73 changes: 64 additions & 9 deletions tests/integration/messages/generated/rflx-universal-message.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,8 +115,14 @@ is
Depends =>
(Ctx => (Buffer, First, Last, Written_Last), Buffer => null);

pragma Warnings (Off, "postcondition does not mention function result");

function Initialized (Ctx : Context) return Boolean with
Ghost;
Ghost,
Post =>
True;

pragma Warnings (On, "postcondition does not mention function result");

procedure Reset (Ctx : in out Context) with
Pre =>
Expand Down Expand Up @@ -246,15 +252,27 @@ is
and then Structural_Valid_Message (Ctx)
and then Data'Length = Byte_Size (Ctx);

pragma Warnings (Off, "postcondition does not mention function result");

function Path_Condition (Ctx : Context; Fld : Field) return Boolean with
Pre =>
Valid_Predecessor (Ctx, Fld);
Valid_Predecessor (Ctx, Fld),
Post =>
True;

pragma Warnings (On, "postcondition does not mention function result");

pragma Warnings (Off, "postcondition does not mention function result");

function Field_Condition (Ctx : Context; Val : Field_Dependent_Value) return Boolean with
Pre =>
Has_Buffer (Ctx)
and Val.Fld in Field'Range
and Valid_Predecessor (Ctx, Val.Fld);
and Valid_Predecessor (Ctx, Val.Fld),
Post =>
True;

pragma Warnings (On, "postcondition does not mention function result");

function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with
Pre =>
Expand All @@ -266,9 +284,15 @@ is
when others =>
True);

pragma Warnings (Off, "postcondition does not mention function result");

function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
Pre =>
Valid_Next (Ctx, Fld);
Valid_Next (Ctx, Fld),
Post =>
True;

pragma Warnings (On, "postcondition does not mention function result");

function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
Pre =>
Expand All @@ -281,9 +305,21 @@ is
when others =>
True);

function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
pragma Warnings (Off, "postcondition does not mention function result");

function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field with
Post =>
True;

pragma Warnings (On, "postcondition does not mention function result");

pragma Warnings (Off, "postcondition does not mention function result");

function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean with
Post =>
True;

function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean;
pragma Warnings (On, "postcondition does not mention function result");

function Valid_Next (Ctx : Context; Fld : Field) return Boolean;

Expand Down Expand Up @@ -332,7 +368,13 @@ is
Pre =>
Has_Buffer (Ctx);

function Incomplete_Message (Ctx : Context) return Boolean;
pragma Warnings (Off, "postcondition does not mention function result");

function Incomplete_Message (Ctx : Context) return Boolean with
Post =>
True;

pragma Warnings (On, "postcondition does not mention function result");

pragma Warnings (Off, "precondition is always False");

Expand Down Expand Up @@ -373,9 +415,15 @@ is
Has_Buffer (Ctx)
and Present (Ctx, F_Data);

pragma Warnings (Off, "postcondition does not mention function result");

function Valid_Length (Ctx : Context; Fld : Field; Length : RFLX_Types.Length) return Boolean with
Pre =>
Valid_Next (Ctx, Fld);
Valid_Next (Ctx, Fld),
Post =>
True;

pragma Warnings (On, "postcondition does not mention function result");

procedure Set_Message_Type (Ctx : in out Context; Val : RFLX.Universal.Message_Type) with
Pre =>
Expand Down Expand Up @@ -1082,6 +1130,8 @@ private

type Cursor_State is (S_Valid, S_Structural_Valid, S_Invalid, S_Incomplete);

pragma Warnings (Off, "postcondition does not mention function result");

function Valid_Value (Val : Field_Dependent_Value) return Boolean is
((case Val.Fld is
when F_Message_Type =>
Expand All @@ -1095,7 +1145,12 @@ private
when F_Values =>
True,
when F_Initial | F_Final =>
False));
False))
with
Post =>
True;

pragma Warnings (On, "postcondition does not mention function result");

type Field_Cursor (State : Cursor_State := S_Invalid) is
record
Expand Down
Loading