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.

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

Ensure that session state is not changed by user-defined function #1032

Closed
treiher opened this issue May 13, 2022 · 3 comments
Closed

Ensure that session state is not changed by user-defined function #1032

treiher opened this issue May 13, 2022 · 3 comments
Labels
generator Related to generator package (SPARK code generation)

Comments

@treiher
Copy link
Collaborator

treiher commented May 13, 2022

The private part of the session context contains the current state of the state machine and the state of the memory allocator. The context is a tagged type.

   type Private_Context is private;

   type Context is abstract tagged limited
      record
         P : Private_Context;
      end record;

private

   type Private_Context is
      record
         Next_State : State := S_Start;
         Slots : Test.Session_Allocator.Slots;
         Memory : Test.Session_Allocator.Memory;
      end record;

User-defined functions are realized as abstract primitives. It must be ensured that a user-defined function does not modify the private part of a session context. Unfortunately, using the Old attribute is not possible in that case:

   procedure Foo (Ctx : in out Context; Bar : RFLX.Test.Baz; RFLX_Result : out Boolean) is abstract with
     Post'Class =>
       Ctx.P = Ctx.P'Old;
rflx-test-session.ads:30:08: error: equality on access types is not allowed in SPARK
   30 |       Ctx.P = Ctx.P'Old;
      |       ^~~~~~~~~~~~~~~~~
  violation of aspect SPARK_Mode at line 16
   16 |  SPARK_Mode
      |  ^ here

rflx-test-session.ads:30:16: error: prefix of "Old" attribute which is not a function call is not allowed in SPARK (SPARK RM 3.10(13))
   30 |       Ctx.P = Ctx.P'Old;
      |               ^~~~~
  violation of aspect SPARK_Mode at line 16
   16 |  SPARK_Mode
      |  ^ here
@treiher treiher added the generator Related to generator package (SPARK code generation) label May 13, 2022
@jklmnn
Copy link
Member

jklmnn commented Aug 23, 2022

One problem with this behavior is that it prevents the proof of the remaining unit. To work around this maybe a ghost variable with an assume can be used in the following way:

   Ghost_Context : Private_Context with Ghost;
begin
   Ghost_Context := Ctx.P;
   Foo (Ctx, Result);
   pragma Assume (Ctx.P = Ghost_Context);

One problem is that we might run into the same problem as above that equality on access types is not allowed in SPARK.

@jklmnn
Copy link
Member

jklmnn commented Aug 23, 2022

After an offline discussion we came to the conclusion that we cannot prove that the private part of a context is unchanged after a platform function call. This change could happen by calling Tick on the context in the platform function. The correct way to go here is to check all required properties after each platform function call.

@treiher
Copy link
Collaborator Author

treiher commented Aug 14, 2024

Fixed in 7c29a5a.

@treiher treiher closed this as completed Aug 14, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
generator Related to generator package (SPARK code generation)
Projects
None yet
Development

No branches or pull requests

2 participants