-
Notifications
You must be signed in to change notification settings - Fork 6
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.
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
Access data of refinement layers #535
Comments
Hi @JanSurft, thanks for your question! The general answer to your question is: no. When designing RecordFlux, we wanted to make the specifications as independent as possible so protocols could be combined freely (which also had some unpleasant consequences for generating the provable SPARK code). If TCP had knowledge of IPv4 directly, using the unmodified specification for IPv6 could be a challange. That being said, we have not missed such a feature so far. I'd be interested to know what problem you're trying to solve by e.g. passing information from IPv4 to TCP (tbh, I'm not sure, yet). Maybe some different mechanism could be used indeed... |
Hi @senier, thanks for your quick and informative response! The way you enable binding layers (or message-types) together is great! The decoupled way of binding them in an external statement looks like a great solution and fixes inflexibility problems. But let me broaden my example a bit to make it clearer what I think about, this time with fictive protocol specifications: In Listing 1 There are two "layers": Now in So my natural wish was, that I could parametrize the messages themselves and pass information into those parametric Now maybe the messages can be specified in another way, so that things like that could work anyway. But I couldn't think about any approach that keeps this flexibility of binding different layers in future revisions of the protocol. Listing 1: HamOnEggs: package Common is
type Unsigned8 is range 0 .. 2**8 - 1 with Size => 8;
type Unsigned16 is range 0 .. 2**16 - 1 with Size => 16;
end Common;
---------------------------------------------------------------------------
package Ham is
type Pdu is message
length: Common.Unsigned16
subtype: Common.Unsigned8
then data
with Length => (length - 2) / 8 * 8;
someDummyInformation: Common.Unsigned16;
data: Opaque;
end message;
end Ham;
---------------------------------------------------------------------------
package Eggs is
type Pdu is message
optionFoo: Common.Unsigned8
optionBar: Common.Unsigned8
then infoBlocks
with Length => -- here I would like to reference the length from the Ham parent
infoBlocks: Opaque;
end message;
end Eggs;
---------------------------------------------------------------------------
package HamOnEggs is
for Ham.Pdu use (data => Eggs.Pdu)
if type = 0;
end HamOnEggs; Listing 2: Parametric HamOnEggs (pseudo-syntax): package ParametricEggs is
type Pdu<length: Common.Unsigned16> is message
optionFoo: Common.Unsigned8
optionBar: Common.Unsigned8
then infoBlocks
with Length => length
infoBlocks: Opaque;
end message;
end ParametricEggs;
package HamOnEggsParametrized is
for Ham.Pdu use (data => Eggs.Pdu<length - 2>)
if type = 0;
end HamOnEggsParametrized; |
Nice example ;) The property you want is easy to accomplish by using the special package Common is
type Unsigned8 is range 0 .. 2**8 - 1 with Size => 8;
type Unsigned16 is range 0 .. 2**16 - 1 with Size => 16;
end Common; (The with Common;
package Ham is
type PDU is
message
Length : Common::Unsigned16;
Sub_Type : Common::Unsigned8;
Some_Dummy_Information : Common::Unsigned16;
Data : Opaque
with Size => (Length - 2) / 8 * 8
if Length >= 48;
end message;
end Ham; The size of with Common;
package Eggs is
type PDU is
message
Option_Foo : Common::Unsigned8;
Option_Bar : Common::Unsigned8;
Info_Blocks : Opaque
with Size => Message'Size - (Option_Bar'Last - Option_Foo'First + 1);
end message;
end Eggs; When you refine with Ham;
with Eggs;
package In_Ham is
for Ham::Pdu use (Data => Eggs::PDU)
if Sub_Type = 0;
end In_Ham; Does that cover your scenario? If you had something different in mind (and the length just happened to be your example), don't hesitate to extend your example specs. |
@JanSurft Did this answer your question? If so, then please close the issue. Don't hesitate to open another ticket if necessary. |
Is it possible to access data of refinement layers in any way?
A simple pseudo example (just for the meaning and usecase):
Now I would like to access the IP Header within the TCP packet... like passing information from the source (IPv4) to the target (TCP) is that possible in any way? Or is there another facility that allows accessing information of "other layers"?
The text was updated successfully, but these errors were encountered: