Skip to content

Commit

Permalink
Add support for No_Secondary_Stack restriction
Browse files Browse the repository at this point in the history 
Ref. #911
  • Loading branch information
@treiher
treiher committed Jan 27, 2022
1 parent ee50196 commit 1222c60
Show file tree
Hide file tree
Showing 125 changed files with 2,172 additions and 905 deletions.
5 changes: 3 additions & 2 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ format:
black -l 100 $(python-packages) ide/gnatstudio
isort $(python-packages) ide/gnatstudio

test: test_python_coverage test_python_property test_spark test_apps test_specs test_runtime test_installation
test: test_python_coverage test_python_property test_spark test_apps test_compilation test_specs test_runtime test_installation

test_python:
python3 -m pytest -n$(shell nproc) -vv -m "not hypothesis" tests
Expand Down Expand Up @@ -84,6 +84,7 @@ test_apps:
$(MAKE) -C examples/apps/dhcp_client test

test_compilation:
$(MAKE) -C tests/spark build_strict
$(MAKE) -C tests/spark test
$(MAKE) -C examples/apps/ping build
$(MAKE) -C examples/apps/dhcp_client build
Expand All @@ -98,7 +99,7 @@ test_runtime:
$(MAKE) -C build/ada-runtime
mkdir -p build/aunit
echo "project AUnit is end AUnit;" > build/aunit/aunit.gpr
cd tests/spark && gprbuild -Ptest --RTS=../../build/ada-runtime/build/posix/obj -Xtype=unchecked -aP ../../build/aunit
cd tests/spark && gprbuild -Ptest --RTS=../../build/ada-runtime/build/posix/obj -Xmode=runtime_compatible -aP ../../build/aunit

test_installation:
rm -rf $(build-dir)/venv
Expand Down
2 changes: 2 additions & 0 deletions defaults.adc
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
pragma Restrictions (No_Elaboration_Code);
pragma Restrictions (No_Secondary_Stack);
9 changes: 9 additions & 0 deletions defaults.gpr
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
abstract project Defaults is

type Build_Mode is ("strict", "asserts_enabled", "optimized", "runtime_compatible");
Mode : Build_Mode := external ("mode", "strict");

Compiler_Variant := external ("gnat", "");

GNATVI := "-gnatVi"; -- ISSUE: Componolit/Workarounds#43
Expand All @@ -22,6 +25,12 @@ abstract project Defaults is
when others =>
end case;

case Mode is
when "strict" =>
GNATA := "";
when "asserts_enabled" | "optimized" | "runtime_compatible" =>
end case;

Proof_Switches :=
(
"--prover=z3,cvc4,altergo",
Expand Down
30 changes: 30 additions & 0 deletions rflx/expression.py
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
# pylint: disable=too-many-lines,too-many-ancestors,too-many-arguments

from __future__ import annotations

import difflib
import itertools
import operator
Expand Down Expand Up @@ -1513,6 +1516,33 @@ def substituted(
)


class Slice(Name):
"""Only used by code generator and therefore provides minimum functionality."""

def __init__(self, prefix: Expr, first: Expr, last: Expr) -> None:
self.prefix = prefix
self.first = first
self.last = last
super().__init__()

def __neg__(self) -> Name:
raise NotImplementedError

def _check_type_subexpr(self) -> RecordFluxError:
raise NotImplementedError

@property
def representation(self) -> str:
return f"{self.prefix} ({self.first} .. {self.last})"

def ada_expr(self) -> ada.Expr:
return ada.Slice(self.prefix.ada_expr(), self.first.ada_expr(), self.last.ada_expr())

@lru_cache(maxsize=None)
def z3expr(self) -> z3.ExprRef:
raise NotImplementedError


class UndefinedExpr(Name):
@property
def representation(self) -> str:
Expand Down
62 changes: 41 additions & 21 deletions rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -393,7 +393,7 @@ def __create_message(self, message: Message) -> None:
unit += self.__create_byte_size_function()
unit += self.__create_message_last_function()
unit += self.__create_written_last_function()
unit += self.__create_message_data_function()
unit += self.__create_message_data_procedure()
unit += self.__create_path_condition_function(message)
unit += self.__create_field_condition_function(message)
unit += self.__create_field_size_function(message, scalar_fields, composite_fields)
Expand Down Expand Up @@ -435,9 +435,7 @@ def __create_message(self, message: Message) -> None:
message, fields_with_explicit_size, fields_with_implicit_size
)
unit += self.__serializer.create_opaque_setter_procedures(message)
unit += self.__serializer.create_generic_opaque_setter_procedures(
message, fields_with_implicit_size
)
unit += self.__serializer.create_generic_opaque_setter_procedures(message)

unit += self.__create_switch_procedures(message, sequence_fields)
unit += self.__create_complete_functions(message, sequence_fields)
Expand Down Expand Up @@ -1359,6 +1357,7 @@ def __create_read_function() -> UnitPart:
SubprogramDeclaration(
specification,
[
Ghost(),
Precondition(
AndThen(
Call("Has_Buffer", [Variable("Ctx")]),
Expand Down Expand Up @@ -1442,7 +1441,18 @@ def __create_generic_read_procedure() -> UnitPart:
specification,
[],
[
CallStatement("Read", [Call("Read", [Variable("Ctx")])]),
CallStatement(
"Read",
[
Indexed(
Variable("Ctx.Buffer.all"),
ValueRange(
Call(const.TYPES_TO_INDEX, [Variable("Ctx.First")]),
Call(const.TYPES_TO_INDEX, [Variable("Ctx.Verified_Last")]),
),
)
],
),
],
)
],
Expand Down Expand Up @@ -2563,9 +2573,10 @@ def __create_written_last_function() -> UnitPart:
)

@staticmethod
def __create_message_data_function() -> UnitPart:
specification = FunctionSpecification(
"Message_Data", const.TYPES_BYTES, [Parameter(["Ctx"], "Context")]
def __create_message_data_procedure() -> UnitPart:
specification = ProcedureSpecification(
"Message_Data",
[Parameter(["Ctx"], "Context"), OutParameter(["Data"], const.TYPES_BYTES)],
)

return UnitPart(
Expand All @@ -2577,25 +2588,34 @@ def __create_message_data_function() -> UnitPart:
AndThen(
Call("Has_Buffer", [Variable("Ctx")]),
Call("Structural_Valid_Message", [Variable("Ctx")]),
)
),
Postcondition(
Equal(
Length(Result(specification.identifier)),
Call("Byte_Size", [Variable("Ctx")]),
Equal(
Length("Data"),
Call(
"Byte_Size",
[
Variable("Ctx"),
],
),
),
)
),
],
),
],
private=[
ExpressionFunctionDeclaration(
[
SubprogramBody(
specification,
Slice(
Variable("Ctx.Buffer.all"),
Call(const.TYPES_TO_INDEX, [Variable("Ctx.First")]),
Call(const.TYPES_TO_INDEX, [Variable("Ctx.Verified_Last")]),
),
[],
[
Assignment(
"Data",
Slice(
Variable("Ctx.Buffer.all"),
Call(const.TYPES_TO_INDEX, [Variable("Ctx.First")]),
Call(const.TYPES_TO_INDEX, [Variable("Ctx.Verified_Last")]),
),
)
],
)
],
)
Expand Down
2 changes: 2 additions & 0 deletions rflx/generator/parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
FormalSubprogramDeclaration,
FunctionSpecification,
GenericFunctionInstantiation,
Ghost,
GreaterEqual,
If,
IfStatement,
Expand Down Expand Up @@ -797,6 +798,7 @@ def specification(field: Field) -> FunctionSpecification:
SubprogramDeclaration(
specification(f),
[
Ghost(),
Precondition(
AndThen(
Call("Has_Buffer", [Variable("Ctx")]),
Expand Down
91 changes: 58 additions & 33 deletions rflx/generator/serializer.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -779,14 +779,11 @@ def specification(field: Field) -> ProcedureSpecification:
],
)

def create_generic_opaque_setter_procedures(
self,
message: Message,
fields_with_implicit_size: List[Field],
) -> UnitPart:
def create_generic_opaque_setter_procedures(self, message: Message) -> UnitPart:
def specification(field: Field) -> ProcedureSpecification:
return ProcedureSpecification(
f"Generic_Set_{field.name}", [InOutParameter(["Ctx"], "Context")]
f"Generic_Set_{field.name}",
[InOutParameter(["Ctx"], "Context"), Parameter(["Length"], const.TYPES_LENGTH)],
)

def formal_parameters(field: Field) -> List[FormalSubprogramDeclaration]:
Expand All @@ -801,7 +798,7 @@ def formal_parameters(field: Field) -> List[FormalSubprogramDeclaration]:
),
FormalSubprogramDeclaration(
FunctionSpecification(
"Valid_Length",
"Process_Data_Pre",
"Boolean",
[Parameter(["Length"], const.TYPES_LENGTH)],
)
Expand All @@ -820,18 +817,30 @@ def formal_parameters(field: Field) -> List[FormalSubprogramDeclaration]:
Call(
"Valid_Length",
[
Call(
const.TYPES_TO_LENGTH,
[
Call(
"Field_Size",
[
Variable("Ctx"),
Variable(f.affixed_name),
],
),
],
),
Variable("Ctx"),
Variable(f.affixed_name),
Variable("Length"),
],
),
GreaterEqual(
Call(
const.TYPES_TO_LENGTH,
[
Call(
"Available_Space",
[
Variable("Ctx"),
Variable(f.affixed_name),
],
),
],
),
Variable("Length"),
),
Call(
"Process_Data_Pre",
[
Variable("Length"),
],
),
)
Expand All @@ -846,14 +855,39 @@ def formal_parameters(field: Field) -> List[FormalSubprogramDeclaration]:
formal_parameters(f),
)
for f, t in message.field_types.items()
if isinstance(t, Opaque) and f not in fields_with_implicit_size
if isinstance(t, Opaque)
],
[
SubprogramBody(
specification(f),
[
*common.field_bit_location_declarations(Variable(f.affixed_name)),
*self.__field_byte_location_declarations(),
ObjectDeclaration(
["First"],
const.TYPES_BIT_INDEX,
Call("Field_First", [Variable("Ctx"), Variable(f.affixed_name)]),
constant=True,
),
ObjectDeclaration(
["Buffer_First"],
const.TYPES_INDEX,
Call(const.TYPES_TO_INDEX, [Variable("First")]),
constant=True,
),
ObjectDeclaration(
["Buffer_Last"],
const.TYPES_INDEX,
Call(
const.TYPES_TO_INDEX,
[
Add(
Variable("First"),
Call(const.TYPES_TO_BIT_LENGTH, [Variable("Length")]),
-Number(1),
)
],
),
constant=True,
),
],
[
CallStatement(
Expand All @@ -870,22 +904,13 @@ def formal_parameters(field: Field) -> List[FormalSubprogramDeclaration]:
f"Initialize_{f.name}_Private",
[
Variable("Ctx"),
Call(
const.TYPES_LENGTH,
[
Add(
Variable("Buffer_Last"),
-Variable("Buffer_First"),
Number(1),
),
],
),
Variable("Length"),
],
),
],
)
for f, t in message.field_types.items()
if isinstance(t, Opaque) and f not in fields_with_implicit_size
if isinstance(t, Opaque)
],
)

Expand Down
Loading

0 comments on commit 1222c60

Please sign in to comment.