Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Initial support of protocol sessions in SPARK #292

Closed
senier opened this issue Jun 17, 2020 · 4 comments · Fixed by #704
Closed

Initial support of protocol sessions in SPARK #292

senier opened this issue Jun 17, 2020 · 4 comments · Fixed by #704
Assignees
@treiher
Labels
generator Related to generator package (SPARK code generation)
Projects
RecordFlux 0.5

Comments

@senier
Copy link
Member

senier commented Jun 17, 2020 •
edited by treiher
Loading

Generate SPARK code for the protocol sessions added in #47.

  • Protocol sessions
    • Declarations
      • Renaming declaration
      • Variable declaration
        • Initialization expressions
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • No initialization
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Types
          • Message
          • Message sequence
          • Scalar
          • Scalar sequence
    • Expressions
      • Aggregates
        • Expressions
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Types
          • Message
          • Scalar
      • Attribute expressions
        • Head attribute
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Message sequence
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Scalar sequence
          • Variables
          • Valid attributes
        • Has_data attribute
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Opaque attribute
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Valid attribute
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
      • Bindings
        • Aggregates
        • Bindings
        • Calls
        • Conversions
        • Head attributes
        • Has_data attributes
        • Literals
        • List comprehensions
        • Message aggregates
        • Mathematical expressions
        • Opaque attributes
        • Quantified expressions
        • Selected expressions
        • Variables
        • Valid attributes
      • Calls
        • Aggregates
        • Bindings
        • Calls
        • Conversions
        • Head attributes
        • Has_data attributes
        • Literals
        • List comprehensions
        • Message aggregates
        • Mathematical expressions
        • No argument
        • Opaque attributes
        • Quantified expressions
        • Selected expressions
        • Variables
        • Valid attributes
      • Conversions
        • Aggregates
        • Bindings
        • Calls
        • Conversions
        • Head attributes
        • Has_data attributes
        • Literals
        • List comprehensions
        • Message aggregates
        • Mathematical expressions
        • Opaque attributes
        • Quantified expressions
        • Selected expressions
        • Variables
        • Valid attributes
      • List comprehensions
        • Assignment statements
        • Condition: selected
        • Global declarations
        • Local declarations
        • Source: selected
        • Source sequence as target
        • Source: message sequence
        • Source: scalar sequence
        • State transitions
        • Target: message sequence
        • Target: scalar sequence
        • Source: variable
      • Quantified expressions
        • Iterable expressions
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Predicate expressions
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
      • Selected expressions
        • Aggregates
        • Bindings
        • Calls
        • Conversions
        • Head attributes
        • Has_data attributes
        • Literals
        • List comprehensions
        • Message aggregates
        • Mathematical expressions
        • Opaque attributes
        • Quantified expressions
        • Selected expressions
        • Variables
        • Valid attributes
    • Session parameters
      • Channels
        • Readable
        • Readable and writable
        • Writable
      • Functions
        • Allowed parameter types
          • Definite messages
          • Opaque fields of messages
          • Scalars
        • Allowed return types
          • Definite messages
          • Scalars
      • Private types
    • States
      • State actions
        • Assignment statements
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Append attribute statements
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Extend attribute statements
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Read attribute statements
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Reset attribute statements
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
        • Write attribute statements
          • Aggregates
          • Bindings
          • Calls
          • Conversions
          • Head attributes
          • Has_data attributes
          • Literals
          • List comprehensions
          • Message aggregates
          • Mathematical expressions
          • Opaque attributes
          • Quantified expressions
          • Selected expressions
          • Variables
          • Valid attributes
      • State declarations
        • Variable declarations
          • Initialization expressions
            • Aggregates
            • Bindings
            • Calls
            • Conversions
            • Head attributes
            • Has_data attributes
            • Literals
            • List comprehensions
            • Message aggregates
            • Mathematical expressions
            • No initialization
            • Opaque attributes
            • Quantified expressions
            • Selected expressions
            • Variables
            • Valid attributes
          • Types
            • Message
            • Message sequence
            • Scalar
            • Scalar sequence
      • Exception transition
      • Null state
      • State transitions
        • Aggregates
        • Bindings
        • Calls
        • Conversions
        • Head attributes
        • Has_data attributes
        • Literals
        • List comprehensions
        • Message aggregates
        • Mathematical expressions
        • No condition
        • Opaque attributes
        • Quantified expressions
        • Selected expressions
        • Variables
        • Valid attributes
@senier senier created this issue from a note in RecordFlux 0.5 (To do) Jun 17, 2020
@senier senier added the generator Related to generator package (SPARK code generation) label Jun 17, 2020
@treiher treiher self-assigned this Oct 23, 2020
@treiher treiher moved this from To do to In progress in RecordFlux 0.5 Oct 23, 2020
@treiher
Copy link
Collaborator

treiher commented Feb 2, 2021 •
edited by senier
Loading

I1: Ensuring validity of sequence elements in list comprehensions

      state Receive_Ack is
         Ack_Message_Types : DHCP_Message_Types;
      begin
         Channel'Read (Ack);  -- sequence field `Ack.Options` could contain invalid elements
         Ack_Message_Types := [for O in Ack.Options => O.DHCP_Message_Type when O.Code = DHCP::DHCP_MESSAGE_TYPE_OPTION];

Considered Options

O1: Use exception transition

+ Easy to realize
- Exceptions shouldn't be used for control flow
- Invalid messages are indistinguishable from internal errors

O2: Check validity of sequence and switch state dependent on result

  • O2.1: Check sequence before list comprehension
  • O2.2: Check resulting sequence after list comprehension (considering result as optional type)

- Requires preconditions for states
- Elaborate specification verification

O3: Hierarchical state machine

  • Use separate sub-states for checking sequence and accessing sequence elements
  • Properties of validity checking could be kept in SPARK by inlining the procedures which represent sub-states

+ Solves also other problems (e.g., global variables)
- Major change of model

Decision Outcome

Long term: O3
Short term: O1

I2: Ensuring successful access to optional message fields

For optional message fields the access to a message field M.F can fail even if M'Valid was checked.

      state A is
         Foo : Field_Type;
      begin
         Channel'Read (Some_Message);
         Foo := Some_Message.Foo;  -- `Foo` could be an optional field and not present in `Some_Message`

Considered Options

O1: Implicitly check validity of message field and use exception transition in case of invalid field

+ Easy to realize
- Exceptions shouldn't be used for control flow
- Invalid messages are indistinguishable from internal errors

O2: Hierarchical state machine and 'Valid attribute for message fields

  • Use separate sub-states for checking validity of message field and accessing field value
  • Properties of validity checking could be kept in SPARK by inlining the procedures which represent sub-states

+ Solves also other problems (e.g., global variables)
- Major change of model

Decision Outcome

Long term: O2
Short term: O1

I3: Ensuring successful access to (optional) message fields in sequences (combination of I1 and I2)

      state Receive_Ack is
         Message_Types : Message_Types;
      begin
         Channel'Read (M);  -- sequence field `M.Values` could contain invalid elements
         Message_Types := [for V in M.Values => V.Message_Type when M.Code = Test::Msg];  -- `Message_Type` could be an optional field and not present in `V`

Decision Outcome

Same as for I1 and I2.

This was referenced Feb 2, 2021
Open
Closed
@treiher treiher mentioned this issue Feb 12, 2021
Closed
3 tasks
treiher added a commit that referenced this issue Feb 15, 2021
@treiher
Add calculation of message size based on field values
0091123 
Ref. #292
treiher added a commit that referenced this issue Feb 15, 2021
@treiher
Add procedure for resetting state of sequence context
acbf1ac 
Ref. #292
treiher added a commit that referenced this issue Mar 30, 2021
@treiher
Add calculation of message size based on field values
ef67206 
Ref. #292
treiher added a commit that referenced this issue Mar 30, 2021
@treiher
Add procedure for resetting state of sequence context
6efae31 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Enable deallocation of Bytes_Ptr
348221e 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Enable getting available space in sequence context
9339314 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Add procedure for resetting state of sequence context
136a9a6 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Enable copying of messages
35cfcaa 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Enable reading, writing and resetting of messages
aa43444 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Refactor generator
13556ab 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Remove Ghost aspects
4c4066a 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Remove Inline_For_Proof annotations
b8c6646 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Fix code generation for messages
01ef671 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Ensure alignment of messages before context initialization
9b5ad1a 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Ensure alignment of messages in generated code
723e5f6 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Restrict copying to valid sequences
56f6d9a 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Restrict copying to structural valid messages
367c7c9 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Improve provability
602b53b 
Ref. #292
treiher added a commit that referenced this issue Mar 31, 2021
@treiher
Update proof session files
d35d2e5 
Ref. #292
@treiher treiher mentioned this issue Mar 31, 2021
Closed
treiher added a commit that referenced this issue Apr 1, 2021
@treiher
Enable getting available space in sequence context
4600e62 
Ref. #292
treiher added a commit that referenced this issue Apr 1, 2021
@treiher
Add procedure for resetting state of sequence context
bb0427f 
Ref. #292
treiher added a commit that referenced this issue Jul 23, 2021
@treiher
Add code generation for sessions
b02bc4b 
Ref. #292
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Remove session specification for TLS handshake protocol
f85752f 
Ref. #292
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Remove session specification for TLS record layer
2c7e988 
Ref. #292
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Add unit tests
7e34e6f 
Ref. #292
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Improve check message in case of wrong instantation
cab5dd4 
Ref. #292
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Add tool for tracing requirements
bf9d17c 
Ref. #292
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Add code generation for sessions
faec29b 
Ref. #292
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Enable controlling debug output in generated code using CLI
0a0f6a9 
Ref. #292
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Consider exception transitions in reachabililty analysis
a8a465a 
Ref. #292
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Improve language reference
a1fbddd 
Ref. #292, #704
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Improve DHCP example app
7a75769 
Ref. #292, #704
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Rename BinAdd to Concatenation
a299018 
Ref. #292, #704
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Improve documentation of session generator
b436967 
Ref. #292, #704
treiher added a commit that referenced this issue Jul 27, 2021
@treiher
Add description of string to language reference
afeef9c 
Ref. #292, #704
RecordFlux 0.5 automation moved this from Under review to Merged Jul 28, 2021
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Remove session specification for TLS handshake protocol
daeedca 
Ref. #292
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Remove session specification for TLS record layer
e85f5a4 
Ref. #292
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Add unit tests
3918019 
Ref. #292
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Improve check message in case of wrong instantation
ba733fe 
Ref. #292
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Add tool for tracing requirements
9bb6f25 
Ref. #292
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Add code generation for sessions
6ad532c 
Ref. #292
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Enable controlling debug output in generated code using CLI
f8a9472 
Ref. #292
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Consider exception transitions in reachabililty analysis
ac7617d 
Ref. #292
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Improve language reference
9f22021 
Ref. #292, #704
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Improve DHCP example app
4ab5440 
Ref. #292, #704
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Rename BinAdd to Concatenation
6ea2770 
Ref. #292, #704
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Improve documentation of session generator
b7f16ab 
Ref. #292, #704
treiher added a commit that referenced this issue Jul 28, 2021
@treiher
Add description of string to language reference
6c7da05 
Ref. #292, #704
@treiher treiher mentioned this issue Aug 4, 2021
Closed
9 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@treiher treiher

Labels
generator Related to generator package (SPARK code generation)
Projects
No open projects
RecordFlux 0.5
  
Merged
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Issue 292, 506, 675, 703, 707: Add initial support of protocol session in SPARK AdaCore/RecordFlux
2 participants
@senier @treiher