How could this code raise a Constraint_Error at runtime?

General
1

Can someone help me understand why GNAT is warning me that the following code could raise a Constraint_Error?

   function Test_Function (Test_Input : Boolean) return Boolean is
   begin
      if Test_Input then
         return False;
      else
         return True;
      end if;
   end Test_Function;

I’m working with a ZFP runtime, with pragma Restrictions (No_Exception_Propagation), and GNAT gives me the following error at compile time:

utilities.adb:22:10: warning: pragma Restrictions (No_Exception_Propagation) in effect [-gnatw.x]
utilities.adb:22:10: warning: "Constraint_Error" may call Last_Chance_Handler [-gnatw.x]

To me it looks impossible for this to ever cause a constraint error, as the compiler would catch any attempt to call the function with a non-Boolean parameter, and the return values are both Boolean literals.

2

Do you also have pragma Normalize_Scalars set?

Boolean is implemented as an enum type Boolean is (False, True); so Normalize_Scalars would initialize it with all bits 1… GCC won’t pack anything smaller than 8 bits unless you tell it not to, so this would be 255, which is definitely not True or False.

There’s a comment about this in the GNAT sources: gcc/gcc/ada/cstand.adb at releases/gcc-15 · gcc-mirror/gcc · GitHub

2 Likes
3

Thanks for your reply!
pragma Normalize_Scalars isn’t set anywhere in my project. If you set it compilation will actually fail, because it looks like the light-rv64imafdc runtime I’m using wasn’t compiled with Normalize_Scalars.

4

Hi and welcome to the forums!

Reading through 3. Using GNAT Pro Features Relevant to High Integrity — GNAT User's Guide Supplement for GNAT Pro Safety-Critical and GNAT Pro High-Security 20.0w documentation, it talks a bit about this in point 3.1. The documentation is a bit old, but it could still prove relevant, specially on how to turn off the errors. However, I have not found any explanation as to why would this code fail or cause an exception… What does gnatprove say if you pass this code there? Use the --level=4 argument so that counterexample are activated and you would get a step by step explanation as to how an exception could take place there.

Best regards,
Fer

5

Well,

I created a testbed and ran your example:

pragma Restrictions (No_Exception_Propagation);

procedure Hello is 

   function Test_Function (Test_Input : Boolean) return Boolean is
   begin
      if Test_Input then
         return False;
      else
         return True;
      end if;
   end Test_Function;

   Fake_Bool : Boolean := True;
begin
   Fake_Bool := Test_Function(Fake_Bool);
   null;
end Hello;

And it compiles with no warnings, issues or complains. GNATprove also says nothing! What compiler version are you using? Could you show all the code?

Best regards,
Fer

6

Are you sure the constraint error is in that function and not one that might be calling it?

7

There really isn’t any more of my code to show.
I’m compiling with gnat_riscv64_elf version 14.2.1, using the light-rv64imafdc runtime. I’m compiling with "-gnatwadehl", so all warnings are treated as errors.

Can you try recreating it with pragma Restrictions (No_Exception_Propagation); enabled? I created a minimal reproducible example, and this restriction is the magic ingredient to triggering the error, which makes sense.

8

No, I’m never actually calling this function. All I need to do to trigger the compilation error is define it. The error points to the line: if Test_Input then.

9

My guess: size of the Test_Input parameter is larger than 1 bit, thus actual value might be out of range. Read more about validity checks

You can ask compiler to generate expanded code using -gnatD switch, and look what compiler do.

10

It is not a magic ingredient, it activates warning when restrictions applied, because exception propagation is not supported by runtime, and last chance handler is called directly. For runtimes with support of exception propagation exception is raised and propagated out of the subprogram.

11

The crazy thing is that you can prove this function correct using SPARK, but when treating warnings as errors, it won’t compile because of the warning about exception propagation.

12

Do you have any validity checks enabled, e.g. -gnatVa?

1 Like
13

Maybe a very nieve answer that skips over the ZFP aspect. Is Test_Input declared and initialized somewhere (in scope/visible to Test_Function) before it’s passed as a parameter into Test_Function, say in a spec/declaration somewhere, if not in the calling code?

If so,
(1) you have the answer without even needing Test_Function.

(2) code is just: function Test_Function(Test_Input: in out boolean) return boolean is…

…

return Test_Input; — ridiculously redundant

As another noted boolean is an enumeration type anyway. Maybe test ZFP some other way and not argue with/or question what the compiler is whining about. For little me, when Mr. Compiler complains, I just listen, and believe it, as it is what it is and does what it does and it’s easier, for me, just to go along and complete my higher goal, when there is one.

14

Yes, I do actually. If you remove this compiler flag the warning isn’t generated.
Thank you for pointing this out! I’ll investigate this further.

The GPR file for this project has been inherited from another old project. I don’t know why these particular compilation switches were chosen. I think they were just chosen to set the strictness to the maximum.

15

Test_Input is a function argument, not a global variable. It’s not set anywhere else. I understand how to suppress the warning by explicitly handling the exception. I’m just confused under what conditions could a boolean generate a Constraint_Error. Is the compiler not assuming that Test_Input has a semantically valid value when the function is called?

16

Here’s another interesting problem I’ve encountered after removing the extra validity checks:

   function Test_Divide (Test_Natural : Natural) return Natural is
   begin
      return Test_Natural / 32;
   exception
      when Constraint_Error =>
         return 0;
   end Test_Divide;

When compiling this code with gnat_riscv64_elf = “^15.2.1”, and the light-rv64imafdc runtime, this code will fail with the following error:
test.adb:19:07: warning: pragma Restrictions (No_Exception_Propagation) in effect [-gnatw.x]
test.adb:19:07: warning: this handler can never be entered, and has been removed [-gnatw.x]

Remove the exception handling block, and it fails with the opposite error:
test.adb:17:27: warning: pragma Restrictions (No_Exception_Propagation) in effect [-gnatw.x]
test.adb:17:27: warning: “Constraint_Error” may call Last_Chance_Handler [-gnatw.x]

Compiling with the native GNAT compiler for Linux x86-64, I don’t encounter this problem. It correctly determines that this code can raise a constraint error at runtime.

What am I missing here? Any pointers would be appreciated.

1 Like
17

Is in out needed with the parameter Test_Natural before you can use Test_Natural as a return value?