Skip to content

Commit

Permalink
Decouple Ada expressions from RecordFlux expressions
Browse files Browse the repository at this point in the history 
Ref. #432
  • Loading branch information
@treiher
treiher committed Sep 9, 2020
1 parent 21aa064 commit 28b0635
Show file tree
Hide file tree
Showing 9 changed files with 1,940 additions and 1,399 deletions.
716 changes: 705 additions & 11 deletions rflx/ada.py
View file

Large diffs are not rendered by default.

430 changes: 149 additions & 281 deletions rflx/expression.py
View file

Large diffs are not rendered by default.

594 changes: 300 additions & 294 deletions rflx/generator/common.py
View file

Large diffs are not rendered by default.

601 changes: 338 additions & 263 deletions rflx/generator/core.py
View file

Large diffs are not rendered by default.

160 changes: 72 additions & 88 deletions rflx/generator/generator.py
View file

Large diffs are not rendered by default.

131 changes: 62 additions & 69 deletions rflx/generator/parser.py
View file
Original file line number Diff line number Diff line change
@@ -1,49 +1,48 @@
from typing import List, Mapping, Sequence, Tuple

import rflx.expression as expr
from rflx.ada import (
FALSE,
TRUE,
Add,
And,
AndThen,
Assignment,
Call,
CallStatement,
Case,
Equal,
Expr,
ExpressionFunctionDeclaration,
FormalSubprogramDeclaration,
FunctionSpecification,
GenericFunctionInstantiation,
If,
IfStatement,
Indexed,
InOutParameter,
Less,
NamedAggregate,
Number,
ObjectDeclaration,
Old,
Or,
Parameter,
Postcondition,
PragmaStatement,
Precondition,
ProcedureSpecification,
Result,
ReturnStatement,
Selected,
Slice,
Subprogram,
SubprogramBody,
SubprogramDeclaration,
UnitPart,
)
from rflx.common import unique
from rflx.expression import (
FALSE,
TRUE,
Add,
And,
AndThen,
Call,
Equal,
Expr,
If,
Indexed,
Less,
NamedAggregate,
Number,
Old,
Or,
Result,
Selected,
Slice,
Variable,
)
from rflx.common import unique
from rflx.identifier import ID
from rflx.model import BUILTINS_PACKAGE, FINAL, INITIAL, Composite, Field, Message, Scalar, Type

Expand Down Expand Up @@ -75,9 +74,7 @@ def create_internal_functions(
composite_fields: Sequence[Field],
) -> UnitPart:
def result(field: Field, message: Message) -> NamedAggregate:
aggregate: List[Tuple[str, Expr]] = [
("Fld", Variable(field.affixed_name, immutable=True))
]
aggregate: List[Tuple[str, Expr]] = [("Fld", Variable(field.affixed_name))]
if field in message.fields and isinstance(message.types[field], Scalar):
aggregate.append(
(
Expand Down Expand Up @@ -108,7 +105,7 @@ def result(field: Field, message: Message) -> NamedAggregate:
Variable("Fld"),
[
(
Variable(f.affixed_name, immutable=True),
Variable(f.affixed_name),
TRUE if f in composite_fields else FALSE,
)
for f in message.fields
Expand Down Expand Up @@ -137,7 +134,7 @@ def result(field: Field, message: Message) -> NamedAggregate:
Case(
Variable("Fld"),
[
(Variable(f.affixed_name, immutable=True), result(f, message))
(Variable(f.affixed_name), result(f, message))
for f in message.fields
],
)
Expand Down Expand Up @@ -243,17 +240,15 @@ def create_verify_procedure(
# Limitation of GNAT Community 2019 / SPARK Pro 20.0
# Provability of predicate is increased by adding part of
# predicate as assert
PragmaStatement(
"Assert", [str(common.message_structure_invariant(message, self.prefix))]
),
PragmaStatement("Assert", [common.message_structure_invariant(message, self.prefix)]),
# WORKAROUND:
# Limitation of GNAT Community 2019 / SPARK Pro 20.0
# Provability of predicate is increased by splitting
# assignment in multiple statements
IfStatement(
[
(
Equal(Variable("Fld"), Variable(f.affixed_name, immutable=True)),
Equal(Variable("Fld"), Variable(f.affixed_name)),
[
Assignment(
Indexed(
Expand Down Expand Up @@ -346,7 +341,6 @@ def create_verify_procedure(
"Predecessor",
Variable(
FINAL.affixed_name,
immutable=True,
),
),
),
Expand All @@ -365,9 +359,7 @@ def create_verify_procedure(
("State", Variable("S_Incomplete")),
(
"Predecessor",
Variable(
FINAL.affixed_name, immutable=True
),
Variable(FINAL.affixed_name),
),
),
)
Expand Down Expand Up @@ -412,9 +404,7 @@ def create_verify_message_procedure(
specification,
[],
[
CallStatement(
"Verify", [Variable("Ctx"), Variable(f.affixed_name, immutable=True)]
)
CallStatement("Verify", [Variable("Ctx"), Variable(f.affixed_name)])
for f in message.fields
],
)
Expand Down Expand Up @@ -588,9 +578,7 @@ def create_structural_valid_message_function(message: Message) -> UnitPart:
[
ExpressionFunctionDeclaration(
specification,
valid_message_condition(message, structural=True)
.substituted(common.substitution(message))
.simplified(),
valid_message_condition(message, structural=True),
)
],
)
Expand All @@ -611,9 +599,7 @@ def create_valid_message_function(message: Message) -> UnitPart:
[
ExpressionFunctionDeclaration(
specification,
valid_message_condition(message)
.substituted(common.substitution(message))
.simplified(),
valid_message_condition(message),
)
],
)
Expand All @@ -633,7 +619,7 @@ def create_incomplete_message_function(message: Message) -> UnitPart:
*[
Call(
"Incomplete",
[Variable("Ctx"), Variable(f.affixed_name, immutable=True)],
[Variable("Ctx"), Variable(f.affixed_name)],
)
for f in message.fields
]
Expand All @@ -658,9 +644,7 @@ def result(field: Field) -> Expr:
"To_Actual",
[
Selected(
Indexed(
Variable("Ctx.Cursors"), Variable(field.affixed_name, immutable=True)
),
Indexed(Variable("Ctx.Cursors"), Variable(field.affixed_name)),
f"Value.{field.name}_Value",
)
],
Expand All @@ -672,9 +656,7 @@ def result(field: Field) -> Expr:
specification(f, t),
[
Precondition(
Call(
"Valid", [Variable("Ctx"), Variable(f.affixed_name, immutable=True)]
),
Call("Valid", [Variable("Ctx"), Variable(f.affixed_name)]),
)
],
)
Expand All @@ -701,7 +683,7 @@ def specification(field: Field) -> ProcedureSpecification:
Call("Has_Buffer", [Variable("Ctx")]),
Call(
"Present",
[Variable("Ctx"), Variable(f.affixed_name, immutable=True)],
[Variable("Ctx"), Variable(f.affixed_name)],
),
)
)
Expand Down Expand Up @@ -729,7 +711,7 @@ def specification(field: Field) -> ProcedureSpecification:
Selected(
Indexed(
Variable("Ctx.Cursors"),
Variable(f.affixed_name, immutable=True),
Variable(f.affixed_name),
),
"First",
)
Expand All @@ -746,7 +728,7 @@ def specification(field: Field) -> ProcedureSpecification:
Selected(
Indexed(
Variable("Ctx.Cursors"),
Variable(f.affixed_name, immutable=True),
Variable(f.affixed_name),
),
"Last",
)
Expand Down Expand Up @@ -774,20 +756,31 @@ def specification(field: Field) -> ProcedureSpecification:
def valid_message_condition(
message: Message, field: Field = INITIAL, structural: bool = False
) -> Expr:
return Or(
*[
l.condition
if l.target == FINAL
else AndThen(
Call(
"Structural_Valid"
if structural and isinstance(message.types[l.target], Composite)
else "Valid",
[Variable("Ctx"), Variable(l.target.affixed_name, immutable=True)],
),
l.condition,
valid_message_condition(message, l.target, structural),
)
for l in message.outgoing(field)
]
def condition(message: Message, field: Field, structural: bool) -> expr.Expr:
return expr.Or(
*[
l.condition
if l.target == FINAL
else expr.AndThen(
expr.Call(
"Structural_Valid"
if structural and isinstance(message.types[l.target], Composite)
else "Valid",
[
expr.Variable("Ctx"),
expr.Variable(l.target.affixed_name, immutable=True),
],
),
l.condition,
condition(message, l.target, structural),
)
for l in message.outgoing(field)
]
)

return (
condition(message, field, structural)
.substituted(common.substitution(message))
.simplified()
.ada_expr()
)
Loading

0 comments on commit 28b0635

Please sign in to comment.