Skip to content

Commit

Permalink
disable inlining via trivial postconditions
Browse files Browse the repository at this point in the history 
To improve gnatprove performance
  • Loading branch information
@kanigsson
kanigsson committed Feb 17, 2022
1 parent 104e0eb commit 92704a2
Show file tree
Hide file tree
Showing 55 changed files with 3,438 additions and 491 deletions.
105 changes: 85 additions & 20 deletions rflx/generator/generator.py
View file
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
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
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
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

0 comments on commit 92704a2

Please sign in to comment.