Add support to ignore suppress pragma #95

xbauch · 2019-01-03T10:25:03Z

Very initial PR at this stage (in terms of full pragma coverage); I think most of those pragmas will be ignored for some time. Pre/post-condition should be implemented if we want to compare to Spark.

martin-cs · 2019-01-08T11:08:42Z

gnat2goto/driver/tree_walk.adb

+              Name_Unsuppress |
+              Name_Volatile |
+              Name_Volatile_Components =>
+            --  These pragmas are currently ignored


I would need to go through the Appendix but I don't think it is safe to ignore all of these.

At the very least the elaboration related pragmas can have an impact on the semantics of an Ada program.

martin-cs · 2019-01-08T19:20:46Z

@xbauch Please see the original issue for a clarification of exactly what is needed. I don't think much of a change is needed.

xbauch · 2019-01-11T16:41:03Z

@martin-cs I went through the documentation, added notes and separeted some cases as unsupported for now.

martin-cs

Mostly just requests for slight reclassifications.

martin-cs · 2019-01-17T15:13:05Z

gnat2goto/driver/tree_walk.adb

-           (if Which in Pragma_Assert | Pragma_Loop_Invariant
-            then I_Code_Assert else I_Code_Assume);
+           (if Which in Pragma_Assume
+            then I_Code_Assume else I_Code_Assert);


This is OK for now but note the open issue on changing these to function calls rather than direct assert / assume.

martin-cs · 2019-01-17T15:15:11Z

gnat2goto/driver/tree_walk.adb

+              Name_Assert_And_Cut |
+            --  Assert and introduce a cut point: the prover can safely forget
+            --  evaluations of local variables and only assume the asserted
+            --  condition. This could be used in symex (making it concolic)


I don't see the link to concolic TBH. Cut points will be handled very differently in this system.

I thought that concolic execution alternates between symex and concrete steps (selecting one evaluation) from which another symex is started. After cut point we continue with only those evaluation satisfying the assertion. It sounds similar to me.

It's an interesting thought. In this context, cut points are meant in the VC generation / Floyd-Hoare style verification sense. In terms of symbolic execution this would be like throwing away the symbolic environment (havocing / non-det-ing all variables) and replacing the path condition with just the assertion. It is an over-approximation step but it is the key thing that makes Floyd-Hoare style verification scalable.

martin-cs · 2019-01-17T15:18:38Z

gnat2goto/driver/tree_walk.adb

              Name_Refined_Depends =>
+            --  We are effectively ignoring the refinement at this point
+            --  Using it would (probably) require modification to CBMC


These should be handled as a "recognised but unsupported pragma" rather than being ignored.

Ok, but we won't be able to run gnat2goto on pretty much any Spark code.

Really? Unless the pragma is used for something else, the refinement things that old-SPARK used to do weren't that commonly used.

Well at least some of the repositories we're considering to for integration testing that use Spark use refining, but maybe not all of them.

Thanks for the head's up; let's solve that problem when we come to it. My understanding was that pragma refine* was a SPARK 2014 construct, rather than an old-SPARK construct and I think much of the code we have planned for integration testing is old-SPARK.

martin-cs · 2019-01-17T15:19:56Z

gnat2goto/driver/tree_walk.adb

+         when Name_Postcondition =>
+            --  Postcondition will eventually also be translated into
+            --  assertions but they should hold elsewhere from where they are
+            --  defined and they refer to 'Result variables


Fair point. I'd rather this was next to the entry for precondition as the handling for them will be similar.

Will it? I though we could deal with precondition as with any other assertion.

... they should eventually become a function call, which we may want to translate into just an assertion, or something else.

The way SPARK uses pre and post conditions is that they are a check (a CPROVER style assert), a cut (as above) and an assume (CPROVER style). Preconditions are assert in the caller, and assume in the callee, postconditions are assert in the callee and assumer in the caller. This allows modular decomposition of the verification process.

Although CPROVER has some support for this kind of thing, we won't be using it by default. So, treat pre and post together and they will become function calls which may then just become asserts, or something more complex.

martin-cs · 2019-01-17T15:21:24Z

gnat2goto/driver/tree_walk.adb

+              Name_Volatile_Components =>
+            --  For a volatile object all reads and updates of the object as a
+            --  whole are performed directly to memory. It changes the
+            --  semantics wrt to thread interleavings.


( Comment not action ) It is also very important to recognise volatile variables during symbolic execution as they are effectively a different variable each time they are accessed.

Even in sequential execution? Do we account for an external system to modify volatile variables (in Ada)?

Yes. Hardware, inter-process shared memory, DMA, etc.

gnat2goto/driver/tree_walk.adb

martin-cs · 2019-01-17T17:26:50Z

@xbauch Thank you for going above and beyond in classifying the pragmas and giving appropriate handling for each. I have a few changes that I would like to these; mostly of the form "Ignoring this is probably the thing to do but at the moment I would like to be warned if these are used".

xbauch · 2019-01-18T10:26:00Z

@martin-cs I changed the wording and re-classified some of the pragmas as requested in the comments. I left the changes in a separate commit (easier reviewing), to be squashed once approved.

sonodtt · 2019-01-21T09:58:31Z

gnat2goto/driver/tree_walk.adb

+                                         "Unsupported pragma: Volatile");
+         when Name_Attach_Handler =>
+            --  The expression in the Attach_Handler pragma as evaluated at
+            --  object creation time specifies an interrupt. s part of the


sonodtt · 2019-01-21T09:58:48Z

gnat2goto/driver/tree_walk.adb

+            --  initialization of that object, if the Attach_Handler pragma is
+            --  specified, the handler procedure is attached to the specified
+            --  interrupt. A check is made that the corresponding interrupt is
+            --  not reserved. We do nut support that check yet.


sonodtt · 2019-01-21T10:11:20Z

gnat2goto/driver/tree_walk.adb

+               CEE := Expressions (Component_Expression);
+               Scope_Size := List_Length (CEE);
+            else
+               Report_Unhandled_Node_Empty (N, "Do_Pragma_Suppress",


Message should be "Do_Pragma_Refine" ?

sonodtt

Many thanks @xbauch for the abundant comments on the pragma types. Some minor typos I've nitpicked on.
There were a few internal sections (Handle_Arg) seem a bit voodoo - I can see how these were handled in the pragma assert, not sure of the differences in the suppress and refine implementations or the rationale.
Maybe a few comments on such in the future? Might cut down on review time.
Regardless, I don't want to get in the way of what's a great body of work, although some sections (as mentioned above) I'm uncertain of without further digging.

sonodtt · 2019-01-21T10:27:10Z

gnat2goto/driver/tree_walk.adb

+
+      begin
+         Iterate_Args (N_Orig);
+         if Scope_Size >= 1


this is essentially equivalent to the use of "if 1" (always true) ?
I guess a scope of size 0 does not make sense.

martin-cs

Thanks for the fixes; please squash and merge once @sonodtt 's issues have been resolved.

Basically into four categories: 1) supported 2) future support 3) ignored -- no semantic effect 4) not supported

xbauch · 2019-01-22T09:17:17Z

@sonodtt thanks for finding the types and pointing to the lack of documentation, I've added a bit about iterating over pragma parameters.

martin-cs requested changes Jan 8, 2019

View reviewed changes

xbauch force-pushed the pragmas branch from db0e132 to 1e3995b Compare January 11, 2019 16:33

martin-cs requested changes Jan 17, 2019

View reviewed changes

xbauch force-pushed the pragmas branch from d592e01 to 58c7837 Compare January 18, 2019 10:24

sonodtt reviewed Jan 21, 2019

View reviewed changes

sonodtt approved these changes Jan 21, 2019

View reviewed changes

sonodtt reviewed Jan 21, 2019

View reviewed changes

martin-cs approved these changes Jan 21, 2019

View reviewed changes

xbauch force-pushed the pragmas branch from 58c7837 to 6876994 Compare January 22, 2019 09:13

Classification of pragmas

63c5f91

Basically into four categories: 1) supported 2) future support 3) ignored -- no semantic effect 4) not supported

xbauch force-pushed the pragmas branch from 6876994 to 63c5f91 Compare January 22, 2019 09:14

xbauch merged commit 69460e6 into diffblue:master Jan 22, 2019

Add support to ignore suppress pragma #95

Add support to ignore suppress pragma #95

Uh oh!

Conversation

xbauch commented Jan 3, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Jan 8, 2019

Uh oh!

xbauch commented Jan 11, 2019

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

martin-cs commented Jan 17, 2019

Uh oh!

xbauch commented Jan 18, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sonodtt left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

xbauch commented Jan 22, 2019

Uh oh!

Uh oh!