Skip to content

Commit

Permalink
Prevent changes of usable range of buffer
Browse files Browse the repository at this point in the history 
- Consider size restrictions of refined fields
- Allow setting array fields with size defined by message size

Ref. #356, #486
  • Loading branch information
@treiher
treiher committed Nov 6, 2020
1 parent aa960e6 commit b2a77fd
Show file tree
Hide file tree
Showing 38 changed files with 1,420 additions and 1,306 deletions.
18 changes: 10 additions & 8 deletions examples/apps/ping/src/icmpv4.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@ is
Success : Boolean;
Ignore_Last : RFLX.RFLX_Builtin_Types.Index;
Buffer : RFLX.RFLX_Builtin_Types.Bytes_Ptr := new RFLX.RFLX_Builtin_Types.Bytes'(1 .. 1024 => 0);
Last : RFLX.RFLX_Builtin_Types.Index;
begin
Socket.Setup;
if
Expand All @@ -79,8 +80,8 @@ is
pragma Loop_Invariant (Buffer /= null);
pragma Loop_Invariant (Buffer'First = 1);
pragma Loop_Invariant (Buffer'Length = 1024);
ICMPv4.Generate (Buffer, Address);
Socket.Send (Buffer.all (Buffer'First .. Buffer'First + 35), Address, Success);
Last := ICMPv4.Generate (Buffer, Address);
Socket.Send (Buffer.all (Buffer'First .. Last), Address, Success);
if not Success then
Ada.Text_IO.Put_Line ("Failed to send packet");
Free_Bytes_Ptr (Buffer);
Expand Down Expand Up @@ -167,13 +168,13 @@ is
-- Generate --
--------------

procedure Generate (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr;
Addr : RFLX.IPv4.Address) is
function Generate (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr;
Addr : RFLX.IPv4.Address) return RFLX.RFLX_Builtin_Types.Index is
use type RFLX.ICMP.Sequence_Number;
use type RFLX.RFLX_Builtin_Types.Bit_Length;
IP_Context : RFLX.IPv4.Packet.Context;
ICMP_Context : RFLX.ICMP.Message.Context;
Data : constant RFLX.RFLX_Builtin_Types.Bytes (1 .. 8) := (others => 65);
Data : constant RFLX.RFLX_Builtin_Types.Bytes (1 .. 56) := (others => 65);
function Valid_Length (L : RFLX.RFLX_Builtin_Types.Length) return Boolean is
(L = Data'Length);
procedure Process_Data (Buffer : out RFLX.RFLX_Builtin_Types.Bytes) with
Expand All @@ -183,15 +184,15 @@ is
begin
Buffer := Data;
end Process_Data;
procedure Set_Data is new RFLX.ICMP.Message.Set_Bounded_Data (Process_Data, Valid_Length);
procedure Set_Data is new RFLX.ICMP.Message.Set_Data (Process_Data, Valid_Length);
begin
pragma Warnings (Off, "unused assignment to ""*_Context""");
RFLX.IPv4.Packet.Initialize (IP_Context, Buf);
RFLX.IPv4.Packet.Set_Version (IP_Context, 4);
RFLX.IPv4.Packet.Set_IHL (IP_Context, 5);
RFLX.IPv4.Packet.Set_DSCP (IP_Context, 0);
RFLX.IPv4.Packet.Set_ECN (IP_Context, 0);
RFLX.IPv4.Packet.Set_Total_Length (IP_Context, 24);
RFLX.IPv4.Packet.Set_Total_Length (IP_Context, 84);
RFLX.IPv4.Packet.Set_Identification (IP_Context, 1);
RFLX.IPv4.Packet.Set_Flag_R (IP_Context, False);
RFLX.IPv4.Packet.Set_Flag_DF (IP_Context, False);
Expand All @@ -214,13 +215,14 @@ is
0, 0, Sequence, Data));
RFLX.ICMP.Message.Set_Identifier (ICMP_Context, 0);
RFLX.ICMP.Message.Set_Sequence_Number (ICMP_Context, Sequence);
Set_Data (ICMP_Context, 64);
Set_Data (ICMP_Context);
RFLX.ICMP.Message.Take_Buffer (ICMP_Context, Buf);
Sequence := Sequence + 1;
else
RFLX.IPv4.Packet.Take_Buffer (IP_Context, Buf);
end if;
pragma Warnings (On, "unused assignment to ""*_Context""");
return RFLX.RFLX_Types.Byte_Index (RFLX.IPv4.Packet.Message_Last (IP_Context));
end Generate;

-----------
Expand Down
7 changes: 3 additions & 4 deletions examples/apps/ping/src/icmpv4.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,15 +26,14 @@ is
SPARK.Heap.Dynamic_Memory),
Input => Ada.Real_Time.Clock_Time);

procedure Generate (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr;
Addr : RFLX.IPv4.Address) with
function Generate (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr;
Addr : RFLX.IPv4.Address) return RFLX.RFLX_Builtin_Types.Index with
Pre => Buf /= null
and then Buf'Length = 1024
and then Buf'First = 1,
Post => Buf /= null
and then Buf'Length = Buf'Length'Old
and then Buf'First = Buf'First'Old,
Global => (In_Out => Ping_State);
and then Buf'First = Buf'First'Old;

procedure Print (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr) with
Pre => Buf /= null
Expand Down
16 changes: 4 additions & 12 deletions rflx/generator/common.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -459,6 +459,8 @@ def invalid_successors_invariant() -> ada.Expr:
]
),
public_context_predicate(),
ada.LessEqual(ada.Variable("First"), ada.Variable("Message_Last")),
ada.LessEqual(ada.Variable("Message_Last"), ada.Variable("Last")),
ada.ForAllIn(
"F",
ada.ValueRange(ada.First("Field"), ada.Last("Field")),
Expand All @@ -480,7 +482,7 @@ def invalid_successors_invariant() -> ada.Expr:
ada.Selected(
ada.Indexed(ada.Variable("Cursors"), ada.Variable("F")), "Last"
),
ada.Variable("Last"),
ada.Variable("Message_Last"),
),
ada.LessEqual(
ada.Selected(
Expand Down Expand Up @@ -576,17 +578,7 @@ def initialize_field_statements(
"Reset_Dependent_Fields",
[ada.Variable("Ctx"), ada.Variable(field.affixed_name)],
),
ada.Assignment(
"Ctx",
ada.Aggregate(
ada.Variable("Ctx.Buffer_First"),
ada.Variable("Ctx.Buffer_Last"),
ada.Variable("Ctx.First"),
ada.Variable("Last"),
ada.Variable("Ctx.Buffer"),
ada.Variable("Ctx.Cursors"),
),
),
ada.Assignment("Ctx.Message_Last", ada.Variable("Last")),
# WORKAROUND:
# Limitation of GNAT Community 2019 / SPARK Pro 20.0
# Provability of predicate is increased by adding part of
Expand Down
97 changes: 39 additions & 58 deletions rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -350,7 +350,7 @@ def __create_generic_message_unit(self, message: Message) -> None:
unit += self.__create_initialized_function(message)
unit += self.__create_take_buffer_procedure(context_invariant)
unit += self.__create_has_buffer_function()
unit += self.__create_message_last_function(message)
unit += self.__create_message_last_function()
unit += self.__create_path_condition_function(message)
unit += self.__create_field_condition_function(message)
unit += self.__create_field_size_function(message)
Expand Down Expand Up @@ -538,6 +538,28 @@ def __create_cursor_type(message: Message) -> UnitPart:

@staticmethod
def __create_context_type() -> UnitPart:
"""
Components of a context type:
Buffer_First, Buffer_Last:
The bounds of `Buffer` which are used to ensure that not a completely different
buffer is moved back into the context.
First, Last:
The positions of the first and last usable bit of `Buffer`. These are hard bounds
which must not be changed during the lifetime of the context.
Message_Last:
The position of the last bit of the message. The value is increased after each
parsed or set field.
Buffer:
An access type refering to memory containing the binary message.
Cursors:
An array of cursors representing the internal parser or serializer state.
"""

discriminants = [
Discriminant(
["Buffer_First", "Buffer_Last"], const.TYPES_INDEX, First(const.TYPES_INDEX)
Expand All @@ -558,6 +580,7 @@ def __create_context_type() -> UnitPart:
RecordType(
"Context",
[
Component("Message_Last", const.TYPES_BIT_INDEX, Variable("First")),
Component("Buffer", const.TYPES_BYTES_PTR, NULL),
Component(
"Cursors",
Expand Down Expand Up @@ -587,6 +610,7 @@ def __create_context_type() -> UnitPart:
Variable("Context.Buffer_Last"),
Variable("Context.First"),
Variable("Context.Last"),
Variable("Context.Message_Last"),
Variable("Context.Buffer"),
Variable("Context.Cursors"),
],
Expand Down Expand Up @@ -660,6 +684,13 @@ def __create_initialize_procedure() -> UnitPart:
[Variable("Ctx.Buffer_First")],
),
),
Equal(
Variable("Ctx.Last"),
Call(
const.TYPES * "Last_Bit_Index",
[Variable("Ctx.Buffer_Last")],
),
),
Call("Initialized", [Variable("Ctx")]),
)
),
Expand Down Expand Up @@ -754,6 +785,7 @@ def __create_restricted_initialize_procedure(message: Message) -> UnitPart:
Variable("Buffer_Last"),
Variable("First"),
Variable("Last"),
Variable("First"),
Variable("Buffer"),
NamedAggregate(
(
Expand Down Expand Up @@ -813,10 +845,7 @@ def __create_initialized_function(message: Message) -> UnitPart:
],
),
Add(
Call(
const.TYPES * "Last_Bit_Index",
[Variable("Ctx.Buffer_Last")],
),
Variable("Ctx.Last"),
-Variable("Ctx.First"),
Number(1),
),
Expand Down Expand Up @@ -1548,62 +1577,14 @@ def __create_valid_predecessor_function(
)

@staticmethod
def __create_message_last_function(message: Message) -> UnitPart:
def __create_message_last_function() -> UnitPart:
specification = FunctionSpecification(
"Message_Last", const.TYPES_BIT_INDEX, [Parameter(["Ctx"], "Context")]
)

return UnitPart(
[
SubprogramDeclaration(
specification,
[
Precondition(
AndThen(
Call("Has_Buffer", [Variable("Ctx")]),
Call("Structural_Valid_Message", [Variable("Ctx")]),
)
)
],
)
],
[
ExpressionFunctionDeclaration(
specification,
If(
[
(
expr.AndThen(
expr.Call(
"Structural_Valid",
[
expr.Indexed(
expr.Variable(expr.ID("Ctx") * "Cursors"),
expr.Variable(
l.source.affixed_name, immutable=True
),
)
],
),
l.condition,
)
.substituted(common.substitution(message))
.simplified()
.ada_expr(),
Selected(
Indexed(
Variable("Ctx.Cursors"),
Variable(l.source.affixed_name),
),
"Last",
),
)
for l in message.incoming(FINAL)
],
Variable(const.TYPES_UNREACHABLE_BIT_LENGTH),
),
)
],
[SubprogramDeclaration(specification)],
[ExpressionFunctionDeclaration(specification, Variable("Ctx.Message_Last"))],
)

@staticmethod
Expand All @@ -1625,7 +1606,7 @@ def __create_available_space_function() -> UnitPart:
ExpressionFunctionDeclaration(
specification,
Add(
Call(const.TYPES_LAST_BIT_INDEX, [Variable("Ctx.Buffer_Last")]),
Variable("Ctx.Last"),
-Call("Field_First", [Variable("Ctx"), Variable("Fld")]),
Number(1),
),
Expand Down Expand Up @@ -2187,7 +2168,7 @@ def __create_valid_context_function(
"Boolean",
[
Parameter(["Buffer_First", "Buffer_Last"], const.TYPES_INDEX),
Parameter(["First", "Last"], const.TYPES_BIT_INDEX),
Parameter(["First", "Last", "Message_Last"], const.TYPES_BIT_INDEX),
AccessParameter(["Buffer"], const.TYPES_BYTES, constant=True),
Parameter(["Cursors"], "Field_Cursors"),
],
Expand Down
3 changes: 3 additions & 0 deletions rflx/generator/parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,9 @@ def create_verify_procedure(
)

set_cursors_statements = [
Assignment(
Variable("Ctx.Message_Last"), Call("Field_Last", [Variable("Ctx"), Variable("Fld")])
),
IfStatement(
[
(
Expand Down

0 comments on commit b2a77fd

Please sign in to comment.