Skip to content

Commit cda85d8

Browse files
committed
Check compatibility rules for exception propagation in ghost code
1 parent 2135404 commit cda85d8

File tree

4 files changed

+180
-11
lines changed

4 files changed

+180
-11
lines changed

docs/lrm/source/exceptions.rst

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,19 @@ Raise Statements and Raise Expressions
2727
Raise statements and raise expressions are in |SPARK|. An exception is said to
2828
be *expected* if it is covered by a choice of an exception handler in an
2929
enclosing handled sequence of statements, or if its enclosing entity is a
30-
procedure body and the exception is covered by a choice in its Exceptional_Cases
31-
aspect whose associated consequence is not statically False.
30+
subprogram body and the exception is covered by a choice in its
31+
Exceptional_Cases aspect whose associated consequence is not statically False.
32+
In addition, if the construct raising the exception is ghost, then it is only
33+
expected if the handled sequence of statements or subprogram body that covers
34+
it fullfils the following properties:
35+
36+
* It shall be ghost,
37+
38+
* it shall be assertion-level-dependent on the construct, and
39+
40+
* if the assertion policy applicable to the construct raising the exception is
41+
Ignore, then the assertion policy applicable to handled sequence of statements
42+
or subprogram body that covers it shall be Ignore too.
3243

3344
As described below, all raise expressions must be provably never executed.
3445
The same holds true for raise statements if they raise unexpected exceptions.

src/spark/spark_util.adb

Lines changed: 22 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3735,7 +3735,6 @@ package body SPARK_Util is
37353735

37363736
function Is_Ghost_With_Respect_To_Context (Call : N_Call_Id) return Boolean
37373737
is
3738-
37393738
function Is_Body (N : Node_Id) return Boolean
37403739
is (Nkind (N) in N_Entity_Body);
37413740

@@ -3745,19 +3744,33 @@ package body SPARK_Util is
37453744
(if Nkind (Call) = N_Function_Call
37463745
then Enclosing_Statement_Of_Call_To_Function_With_Side_Effects (Call)
37473746
else Call);
3748-
begin
3749-
if Is_Ghost_Assignment (Stmt)
3750-
or else Is_Ghost_Declaration (Stmt)
3751-
or else Is_Ghost_Procedure_Call (Stmt)
3752-
then
3747+
Ent : constant Entity_Id :=
3748+
(case Nkind (Stmt) is
3749+
when N_Assignment_Statement =>
3750+
Get_Enclosing_Ghost_Entity (Name (Stmt)),
3751+
when N_Object_Declaration =>
3752+
Defining_Entity (Stmt),
3753+
when N_Procedure_Call_Statement | N_Entry_Call_Statement =>
3754+
Get_Called_Entity (Stmt),
3755+
when others =>
3756+
raise Program_Error);
3757+
3758+
begin
3759+
if not Is_Ghost_Entity (Ent) then
3760+
return False;
3761+
else
37533762
declare
37543763
Caller : constant Entity_Id :=
37553764
Unique_Defining_Entity (Enclosing_Body (Stmt));
37563765
begin
3757-
return not Is_Ghost_Entity (Caller);
3766+
return
3767+
not Is_Ghost_Entity (Caller)
3768+
or else (Is_Checked_Ghost_Entity (Caller)
3769+
and then not Is_Checked_Ghost_Entity (Ent))
3770+
or else not Is_Assertion_Level_Dependent
3771+
(Ghost_Assertion_Level (Caller),
3772+
Ghost_Assertion_Level (Ent));
37583773
end;
3759-
else
3760-
return False;
37613774
end if;
37623775
end Is_Ghost_With_Respect_To_Context;
37633776

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
pragma Assertion_Level (L1);
2+
pragma Assertion_Level (L2, Depends => [L1]);
3+
pragma Assertion_Level (L3);
4+
5+
procedure Main with SPARK_Mode is
6+
pragma Assertion_Policy (Ghost => Ignore);
7+
8+
procedure Raise_PE (B : Boolean)
9+
with
10+
Ghost => Static,
11+
Exceptional_Cases => (Program_Error => B),
12+
Post => not B
13+
is
14+
begin
15+
if B then
16+
raise Program_Error;
17+
end if;
18+
end Raise_PE;
19+
20+
procedure Catch_PE (B : Boolean) with Ghost => Runtime, Post => True is
21+
begin
22+
Raise_PE (B); -- @RAISE:FAIL exception propagated from ignored ghost context to checked ghost context
23+
pragma Assert (Runtime => not B);
24+
exception
25+
when Program_Error =>
26+
null;
27+
end Catch_PE;
28+
29+
procedure Raise_PE_2 (B : Boolean)
30+
with Ghost => L2, Exceptional_Cases => (Program_Error => B), Post => not B
31+
is
32+
begin
33+
if B then
34+
raise Program_Error;
35+
end if;
36+
end Raise_PE_2;
37+
38+
procedure Catch_PE_2 (B : Boolean) with Ghost => L1, Post => True is
39+
begin
40+
Raise_PE_2 (B); -- @RAISE:FAIL exception propagated from incompatible ghost levels
41+
pragma Assert (Runtime => not B);
42+
exception
43+
when Program_Error =>
44+
null;
45+
end Catch_PE_2;
46+
47+
procedure Raise_PE_2_bis (B : Boolean)
48+
with Ghost => L3, Exceptional_Cases => (Program_Error => B), Post => not B
49+
is
50+
begin
51+
if B then
52+
raise Program_Error;
53+
end if;
54+
end Raise_PE_2_bis;
55+
56+
procedure Catch_PE_2_bis (B : Boolean) with Ghost => L1, Post => True is
57+
begin
58+
Raise_PE_2_bis (B); -- @RAISE:FAIL exception propagated from incompatible ghost levels
59+
pragma Assert (Runtime => not B);
60+
exception
61+
when Program_Error =>
62+
null;
63+
end Catch_PE_2_bis;
64+
65+
procedure Raise_PE_3 (B : Boolean)
66+
with Ghost, Exceptional_Cases => (Program_Error => B), Post => not B
67+
is
68+
begin
69+
if B then
70+
raise Program_Error;
71+
end if;
72+
end Raise_PE_3;
73+
74+
procedure Catch_PE_3 (B : Boolean) with Ghost => Runtime, Post => True is
75+
begin
76+
Raise_PE_3 (B); -- @RAISE:FAIL exception propagated from ignored ghost context to checked ghost context
77+
pragma Assert (Runtime => not B);
78+
exception
79+
when Program_Error =>
80+
null;
81+
end Catch_PE_3;
82+
83+
procedure Raise_PE_4
84+
with Ghost => Runtime, Exceptional_Cases => (Program_Error => True), No_Return
85+
is
86+
begin
87+
raise Program_Error;
88+
end Raise_PE_4;
89+
90+
procedure Catch_PE_4 with Ghost, Post => True is
91+
begin
92+
Raise_PE_4; -- OK: exception propagated from checked ghost context to ignored ghost context
93+
exception
94+
when Program_Error =>
95+
null;
96+
end Catch_PE_4;
97+
98+
procedure Raise_PE_5 (B : Boolean)
99+
with Ghost => L1, Exceptional_Cases => (Program_Error => B), Post => not B
100+
is
101+
begin
102+
if B then
103+
raise Program_Error;
104+
end if;
105+
end Raise_PE_5;
106+
107+
procedure Catch_PE_5 (B : Boolean) with Ghost => L2, Post => True is
108+
begin
109+
Raise_PE_5 (B); -- OK: exception propagated from dependent ghost level
110+
pragma Assert (Runtime => not B);
111+
exception
112+
when Program_Error =>
113+
null;
114+
end Catch_PE_5;
115+
begin
116+
Catch_PE (True);
117+
end Main;
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
main.adb:11:45: info: exceptional case proved (CVC5: 1 VC)
2+
main.adb:12:27: info: postcondition proved (CVC5: 1 VC)
3+
main.adb:20:68: info: postcondition proved (Trivial: 1 VC)
4+
main.adb:22:07: medium: unexpected exception might be raised
5+
main.adb:23:33: info: assertion proved (CVC5: 1 VC)
6+
main.adb:30:61: info: exceptional case proved (CVC5: 1 VC)
7+
main.adb:30:73: info: postcondition proved (CVC5: 1 VC)
8+
main.adb:38:65: info: postcondition proved (Trivial: 1 VC)
9+
main.adb:40:07: medium: unexpected exception might be raised
10+
main.adb:41:33: info: assertion proved (CVC5: 1 VC)
11+
main.adb:48:61: info: exceptional case proved (CVC5: 1 VC)
12+
main.adb:48:73: info: postcondition proved (CVC5: 1 VC)
13+
main.adb:56:69: info: postcondition proved (Trivial: 1 VC)
14+
main.adb:58:07: medium: unexpected exception might be raised
15+
main.adb:59:33: info: assertion proved (CVC5: 1 VC)
16+
main.adb:66:55: info: exceptional case proved (CVC5: 1 VC)
17+
main.adb:66:67: info: postcondition proved (CVC5: 1 VC)
18+
main.adb:74:70: info: postcondition proved (Trivial: 1 VC)
19+
main.adb:76:07: medium: unexpected exception might be raised
20+
main.adb:77:33: info: assertion proved (CVC5: 1 VC)
21+
main.adb:84:66: info: exceptional case proved (Trivial: 1 VC)
22+
main.adb:90:45: info: postcondition proved (Trivial: 1 VC)
23+
main.adb:92:07: info: only expected exception raised (CVC5: 1 VC)
24+
main.adb:99:61: info: exceptional case proved (CVC5: 1 VC)
25+
main.adb:99:73: info: postcondition proved (CVC5: 1 VC)
26+
main.adb:107:65: info: postcondition proved (Trivial: 1 VC)
27+
main.adb:109:07: info: only expected exception raised (CVC5: 1 VC)
28+
main.adb:110:33: info: assertion proved (CVC5: 1 VC)

0 commit comments

Comments
 (0)