Static assertions

Static assertions

[Jean-Pierre Rosen]

Still discovering how powerful Ada is...

Imagine your program relies on Integer having a certain size, or being sure
that the size of Integer is four times the size of character, or things like
that, and you want to make sure that the program does not even compile if
the assertions do not hold (because you hate fighting with a debugger). This
is possible, since a static expression that raises constraint_error will not
compile. Just include something like the following package:

package Verifier is
   subtype Assert is Boolean range True..True;

   Assert_1 : constant := Boolean'Pos( Assert (Integer'Size=32) );
   Assert_2 : constant := Boolean'Pos( Assert
(Integer'Size=4*Character'Size) );
end Verifier;

(The Boolean'Pos serves to have a value used in a named number declaration,
which requires a static context).
--
---------------------------------------------------------
           J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr

Re: Static assertions

[Jeffrey Carter]

Jean-Pierre Rosen wrote:
> 
> package Verifier is
>    subtype Assert is Boolean range True..True;
> 
>    Assert_1 : constant := Boolean'Pos( Assert (Integer'Size=32) );
>    Assert_2 : constant := Boolean'Pos( Assert
> (Integer'Size=4*Character'Size) );
> end Verifier;
> 
> (The Boolean'Pos serves to have a value used in a named number declaration,
> which requires a static context).

Interesting. However, Rational Apex 2.4.6 on HP compiles this fine even
if the declarations are changed to make the expressions false. A test
program to output the values of Assert_X produces 2 zeros.

If I change the declarations to

Assert_1 : constant Assert := Integer'Size = 73;

then the unit will not compile.

-- 
Jeffrey Carter

Re: Static assertions

[Marin David Condic]

You have to be careful of the declarations. Just because you maybe did
something to declare (for example) a 16 bit integer type, doesn't mean that
'Size for the type won't end up as 32. Even if you use a rep clause, the
compiler doesn't have to honor it - although one would hope it was at least
polite enough to inform you of that fact.

Perhaps you could post the code you created to test it?

MDC
--
Marin David Condic
Senior Software Engineer
Pace Micro Technology Americas    www.pacemicro.com
Enabling the digital revolution
e-Mail:    marin.condic@pacemicro.com
Web:      http://www.mcondic.com/


"Jeffrey Carter" <jeffrey.carter@boeing.com> wrote in message
news:3B040DE4.468E779F@boeing.com...
> Jean-Pierre Rosen wrote:
> >
> > package Verifier is
> >    subtype Assert is Boolean range True..True;
> >
> >    Assert_1 : constant := Boolean'Pos( Assert (Integer'Size=32) );
> >    Assert_2 : constant := Boolean'Pos( Assert
> > (Integer'Size=4*Character'Size) );
> > end Verifier;
> >
> > (The Boolean'Pos serves to have a value used in a named number
declaration,
> > which requires a static context).
>
> Interesting. However, Rational Apex 2.4.6 on HP compiles this fine even
> if the declarations are changed to make the expressions false. A test
> program to output the values of Assert_X produces 2 zeros.
>
> If I change the declarations to
>
> Assert_1 : constant Assert := Integer'Size = 73;
>
> then the unit will not compile.
>
> --
> Jeffrey Carter

Re: Static assertions

[Jeffrey Carter]

Marin David Condic wrote:
> 
> You have to be careful of the declarations. Just because you maybe did
> something to declare (for example) a 16 bit integer type, doesn't mean that
> 'Size for the type won't end up as 32. Even if you use a rep clause, the
> compiler doesn't have to honor it - although one would hope it was at least
> polite enough to inform you of that fact.
> 
> Perhaps you could post the code you created to test it?

The code was identical to that posted by JPR, except that 32 was changed
to 16, and 4 was changed to 8. This makes both expressions False (for
me, but I would hope at least one of them would be False on every
system). The test program simply used Integer'Image and Put_Line to
output the values of the 2 constants.

> 
> MDC
> --
> Marin David Condic
> Senior Software Engineer
> Pace Micro Technology Americas    www.pacemicro.com
> Enabling the digital revolution
> e-Mail:    marin.condic@pacemicro.com
> Web:      http://www.mcondic.com/
> 
> "Jeffrey Carter" <jeffrey.carter@boeing.com> wrote in message
> news:3B040DE4.468E779F@boeing.com...
> > Jean-Pierre Rosen wrote:
> > >
> > > package Verifier is
> > >    subtype Assert is Boolean range True..True;
> > >
> > >    Assert_1 : constant := Boolean'Pos( Assert (Integer'Size=32) );
> > >    Assert_2 : constant := Boolean'Pos( Assert
> > > (Integer'Size=4*Character'Size) );
> > > end Verifier;
> > >
> > > (The Boolean'Pos serves to have a value used in a named number
> declaration,
> > > which requires a static context).
> >
> > Interesting. However, Rational Apex 2.4.6 on HP compiles this fine even
> > if the declarations are changed to make the expressions false. A test
> > program to output the values of Assert_X produces 2 zeros.
> >
> > If I change the declarations to
> >
> > Assert_1 : constant Assert := Integer'Size = 73;
> >
> > then the unit will not compile.
> >
> > --
> > Jeffrey Carter


-- 
Jeffrey Carter

Re: Static assertions

[Robert A Duff]

"Jean-Pierre Rosen" <rosen@adalog.fr> writes:

>    Assert_1 : constant := Boolean'Pos( Assert (Integer'Size=32) );

Interesting.  But shouldn't it be Assert'(...)?
                                        ^ ie a qualified expression

- Bob

Re: Static assertions

[Christoph Grein]

Robert A Duff wrote:

> Interesting.  But shouldn't it be Assert'(...)?
>                                         ^ ie a qualified expression

  package Verifier is
    subtype Assert is Boolean range True .. True;

    Assert_1 : constant := Boolean'Pos (Assert (Integer'Size = 16));
    Assert_2 : constant := Boolean'Pos
				  (Assert (Integer'Size = 2 * Character'Size));
  end Verifier;

With a type conversion this compiles on my Apex Ada 95 Compiler 3.0.0b on 
Solaris and produces "0 0", with a qualified expression, it gives me the error 
message:

Boolean'Pos (Assert'(Integer'Size = 16)) is disallowed since it is static and 
will raise Constraint_Error [RM_95 4.9(34)]

It seems like the type conversion is ignored.

ARM 4.6(28)
For the evaluation of a type_conversion that is a value conversion, the operand 
is evaluated, and then the value of the operand is converted to a corresponding 
value of the target type, if any. If there is no value of the target type that 
corresponds to the operand value, Constraint_Error is raised[; this can only 
happen on conversion to a modular type, and only when the operand value is 
outside the base range of the modular type.] Additional rules follow:

ARM 4.6(34) Enumeration Type Conversion

ARM 4.6(35)
The result is the value of the target type with the same position number as that 
of the operand value.

Thus there is nowhere specified that the subtype range is checked.
   Put_Line (Integer'Image (Natural (-2.3)));
compiles just fine and produces -2.

ARM 4.7(4)
The evaluation of a qualified_expression evaluates the operand (and if of a 
universal type, converts it to the type determined by the subtype_mark) and 
checks that its value belongs to the subtype denoted by the subtype_mark. The 
exception Constraint_Error is raised if this check fails. 

So thanx to Robert Duff for hinting.

Christoph Grein

Re: Static assertions

[Robert A Duff]

Christoph Grein <christoph.grein@eurocopter.com> writes:

> Robert A Duff wrote:
> 
> > Interesting.  But shouldn't it be Assert'(...)?
> >                                         ^ ie a qualified expression

What I meant was that it's better style to use a qualfied expression
than a type conversion, in cases where both work, because a qual exp is
less powerful.  That is, why say "Warning Will Robinson: I'm converting
types" when you're *not* converting types?

(IMHO a type conversion that converts from a type to itself should cause
at least a warning.)

>   package Verifier is
>     subtype Assert is Boolean range True .. True;
> 
>     Assert_1 : constant := Boolean'Pos (Assert (Integer'Size = 16));
>     Assert_2 : constant := Boolean'Pos
> 				  (Assert (Integer'Size = 2 * Character'Size));
>   end Verifier;
> 
> With a type conversion this compiles on my Apex Ada 95 Compiler 3.0.0b on 

Sounds like a compiler bug, which you should report.  The above code is
illegal (as desired).  The AverCom Ada front end gives two error
messages for the above.

> It seems like the type conversion is ignored.
[... RM exegesis snipped]

You missed 4.6(51), which says that the subtype is checked.  A
type_conversion is really a subtype conversion, despite its name.  That
is, a type_conversion T(X) converts the value of X to the type of
subtype T, and then checks that the value is in the subtype T.

> Thus there is nowhere specified that the subtype range is checked.
>    Put_Line (Integer'Image (Natural (-2.3)));
> compiles just fine and produces -2.

Again, that sounds like a compiler bug.  The AverCom Ada compiler says
it's illegal.

> So thanx to Robert Duff for hinting.

Well, I wasn't hinting at what you thought I was hinting.  ;-)

- Bob

Re: Static assertions

[Marin David Condic]

Well, that settles that one. I thought there was a chance that you might
have been declaring something that was a subtype or derived type or your own
user defined type with a "for 'Size..." clause where just because you said
you wanted 16 bits, doesn't mean you get it. If "Integer'Size=32" is a true
statement, its hard to see "Integer'Size=16" simultaneously being true
except via compiler bug.

MDC
--
Marin David Condic
Senior Software Engineer
Pace Micro Technology Americas    www.pacemicro.com
Enabling the digital revolution
e-Mail:    marin.condic@pacemicro.com
Web:      http://www.mcondic.com/


"Jeffrey Carter" <jeffrey.carter@boeing.com> wrote in message
news:3B0451F7.6D5B7024@boeing.com...
> The code was identical to that posted by JPR, except that 32 was changed
> to 16, and 4 was changed to 8. This makes both expressions False (for
> me, but I would hope at least one of them would be False on every
> system). The test program simply used Integer'Image and Put_Line to
> output the values of the 2 constants.
>

Re: Static assertions

[Jeffrey Carter]

Robert A Duff wrote:
> 
> What I meant was that it's better style to use a qualfied expression
> than a type conversion, in cases where both work, because a qual exp is
> less powerful.  That is, why say "Warning Will Robinson: I'm converting
> types" when you're *not* converting types?

Isn't that "Danger, Will Robinson"?

I certainly agree with this advice. One thing that always stopped me
short in my tracks was code with constructs such

   ... + My_Type (3) - ...

apparently written by people who thought that "3" has type Integer (or
perhaps used a compiler with that "feature").

However, is there any reason to write

   Assert_1 : constant := Boolean'Pos (Assert'(Integer'Size = 73) );

rather than

   Assert_1 : constant Assert := Integer'Size = 73;

? Are there compilers that won't check this during compilation?

-- 
Jeffrey Carter

Re: Static assertions

[Ted Dennison]

In article <3B054ABE.9B3DA459@boeing.com>, Jeffrey Carter says...
>
>Robert A Duff wrote:
>> 
>> less powerful.  That is, why say "Warning Will Robinson: I'm converting
>> types" when you're *not* converting types?
>
>Isn't that "Danger, Will Robinson"?

True, but then again the following:

>One thing that always stopped me
>short in my tracks was code with constructs such

is a bit of a mixed metaphor. Perhaps people who live in glass houses shouldn't
cast the first stone? :-)

---
T.E.D.    homepage   - http://www.telepath.com/dennison/Ted/TED.html
          home email - mailto:dennison@telepath.com

Re: Static assertions

[Robert A Duff]

Jeffrey Carter <jeffrey.carter@boeing.com> writes:

> Isn't that "Danger, Will Robinson"?

Probably.

> I certainly agree with this advice. One thing that always stopped me
> short in my tracks was code with constructs such
> 
>    ... + My_Type (3) - ...
> 
> apparently written by people who thought that "3" has type Integer (or
> perhaps used a compiler with that "feature").

Well, there *are* languages where "3" is an int, and "3L" is
a long (or even "3l").  Yuck.

> However, is there any reason to write
> 
>    Assert_1 : constant := Boolean'Pos (Assert'(Integer'Size = 73) );
> 
> rather than
> 
>    Assert_1 : constant Assert := Integer'Size = 73;
> 
> ? Are there compilers that won't check this during compilation?

I think the former is required to get a compile time error,
whereas the latter is merely allowed to produce a warning.
The subtle difference is that the former has a static expression
raising an exception, whereas the latter has a perfectly good
static expression, but the assignment will raise an exception.
I'm too lazy to look it up in the RM, so I could be mistaken...

Furthermore, if the second one doesn't get detected at compile time, it
might not get detected at all.  I believe 11.6 allows the compiler to
"optimize away" the constraint check, so it never happens at run time.
(I'm assuming Assert_1 is a dead variable.)

- Bob

Re: Static assertions

[Jeffrey Carter]

Robert A Duff wrote:
> 
> Jeffrey Carter <jeffrey.carter@boeing.com> writes:
> 
> > However, is there any reason to write
> >
> >    Assert_1 : constant := Boolean'Pos (Assert'(Integer'Size = 73) );
> >
> > rather than
> >
> >    Assert_1 : constant Assert := Integer'Size = 73;
> >
> > ? Are there compilers that won't check this during compilation?
> 
> I think the former is required to get a compile time error,
> whereas the latter is merely allowed to produce a warning.
> The subtle difference is that the former has a static expression
> raising an exception, whereas the latter has a perfectly good
> static expression, but the assignment will raise an exception.
> I'm too lazy to look it up in the RM, so I could be mistaken...
> 
> Furthermore, if the second one doesn't get detected at compile time, it
> might not get detected at all.  I believe 11.6 allows the compiler to
> "optimize away" the constraint check, so it never happens at run time.
> (I'm assuming Assert_1 is a dead variable.)

I see. Assert_1 cannot be a dead variable, since it is a constant, but
it will probably never be referenced. I guess it's a "dead constant".

It would appear that

   Assert_1 : constant Assert := Assert'(Integer'Size = 73);

must cause a compilation error, since Assert is a static subtype, so the
qualified expression is static, and a static qualified expression must
be evaluated at compile time.

I'm just trying to come up with something a little shorter and less
obscure than using Boolean'Pos.

-- 
Jeffrey Carter

Re: Static assertions

[David Kristola]

On Thu, 17 May 2001 8:07:51 -0700, Jean-Pierre Rosen wrote
(in message <9e0pfb$ao9$1@s1.read.news.oleane.net>):

> package Verifier is
>    subtype Assert is Boolean range True..True;
> 
>    Assert_1 : constant := Boolean'Pos( Assert (Integer'Size=32) );
>    Assert_2 : constant := Boolean'Pos( Assert 
> (Integer'Size=4*Character'Size) ); end Verifier;

Why not

   Assert_1 : constant Assert := (Integer'Size = 32);

?


-- 
   --djk, keeper of arcane lore & trivial fluff
   --Home: David95036 plus 1 at america on-line
   --Spam: goto.hades@welovespam.com

Re: Static assertions

[Aaro Koskinen]

"Jean-Pierre Rosen" <rosen@adalog.fr> writes:
> Still discovering how powerful Ada is...
> 
> Imagine your program relies on Integer having a certain size, or being sure
> that the size of Integer is four times the size of character, or things like
> that, and you want to make sure that the program does not even compile if
> the assertions do not hold (because you hate fighting with a debugger). This
> is possible, since a static expression that raises constraint_error will not
> compile.

I have been using a similar method in C. I have an assert macro, which
declares a const int with the value "1 / <static boolean expression>".
If the assertion does not hold, it evaluates to 0, and the code will
not compile.

-- 
Aaro Koskinen, aaro@iki.fi, http://www.iki.fi/aaro

Re: Static assertions

[Robert A Duff]

Jeffrey Carter <jeffrey.carter@boeing.com> writes:

> I see. Assert_1 cannot be a dead variable, since it is a constant, but
> it will probably never be referenced. I guess it's a "dead constant".

Yeah.  Or "dead object".

> It would appear that
> 
>    Assert_1 : constant Assert := Assert'(Integer'Size = 73);
> 
> must cause a compilation error, since Assert is a static subtype, so the
> qualified expression is static, and a static qualified expression must
> be evaluated at compile time.

I agree.

> I'm just trying to come up with something a little shorter and less
> obscure than using Boolean'Pos.

A worthy goal.  I wish that "Assert(Integer'Size = 73)" would work.
Alas.

- Bob

Re: Static assertions

[Robert A Duff]

David Kristola <David95037@See-My.Sig> writes:

> >    subtype Assert is Boolean range True..True;
> Why not
> 
>    Assert_1 : constant Assert := (Integer'Size = 32);

I said in another post that, unfortunately, this is not required to
cause any compile-time or run-time error.  Sigh.

- Bob

Re: Static assertions

[Jean-Pierre Rosen]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1061 bytes --]


"Aaro Koskinen" <aaro@iki.fi> a �crit dans le message news:
pdx7kzd3fdb.fsf@sirppi.helsinki.fi...
> "Jean-Pierre Rosen" <rosen@adalog.fr> writes:
> > Still discovering how powerful Ada is...
> >
> > Imagine your program relies on Integer having a certain size, or being
sure
> > that the size of Integer is four times the size of character, or things
like
> > that, and you want to make sure that the program does not even compile
if
> > the assertions do not hold (because you hate fighting with a debugger).
This
> > is possible, since a static expression that raises constraint_error will
not
> > compile.
>
> I have been using a similar method in C. I have an assert macro, which
> declares a const int with the value "1 / <static boolean expression>".
> If the assertion does not hold, it evaluates to 0, and the code will
> not compile.
>
Out of curiosity... Is this *required* by the C standard ?

--
---------------------------------------------------------
           J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr

Re: Static assertions

[David Thompson]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 3432 bytes --]

Jean-Pierre Rosen <rosen@adalog.fr> wrote :
>
> "Aaro Koskinen" <aaro@iki.fi> a �crit dans le message news:
> pdx7kzd3fdb.fsf@sirppi.helsinki.fi...
...
> > I have been using a similar method in C. I have an assert macro, which
> > declares a const int with the value "1 / <static boolean expression>".
> > If the assertion does not hold, it evaluates to 0, and the code will
> > not compile.
> >
> Out of curiosity... Is this *required* by the C standard ?
>
Not clearly.  First of all, the 'const' is irrelevant; in (standard) C
a const variable is just readonly, not usable as a compile-time
value = in a "constant expression".  (In C++ a const variable
(initialized in the declaration) or static data member of a class
(initialized in the class definition) of integral or enumeration type
is a compile-time constant, and a combined C/C++ implementation
may provide this in C also as a convenient-to-do extension.)

The initializer for a variable with static duration, which means
all declared at file scope = outside any function, plus those
declared within a function body (block) with the keyword 'static',
must be an arithmetic constant expression convertible to
the correct type (C99 6.7.8p4 was C89/90 6.5.7 constraint)
(but not an "integer[ral] constant expression", which is slightly different).
(For C89/90, the elements of a braced initializer list (for an aggregate)
must also be constant expressions; for C99 they must be so only
for a static variable, for an automatic (stack) variable they need not.)

"Each constant expression shall evaluate to a constant that is in
the range of representable values for its type."  (6.6p4 was 6.4 constraint)
but "The semantic rules for the evaluation of a constant expression
are the same as for a nonconstant expressions" (6.6p11 was 6.4)
and "if the second operand [of / or %] is zero, the behavior is undefined"
(like unbounded error, 6.5.5p5 was 6.3.5, NOT a constraint).
Violating a constraint requires a diagnostic, so the question is
whether the fact that n/0 does not evaluate to a representable
constant (or indeed to any value of type 'int') is "trumped" by
the undefined behavior, which (as used many other places
in the standard) is not clearly defined (!), but is generally held
to relieve the implementation of _all_ obligations imposed.

A safer approach in pure standard C is
  char/*or anything*/ dummy [ boolexpr ];
because in C89/90 the bound in an array declarator
(ignoring the cases where it may be and is omitted)
"shall be an integral constant expression that has a value
greater than zero" (6.5.4.2 constraint) so if it is safely
evaluable and zero it is definitely a required diagnostic.
In C99 (6.7.5.2p1) this is complicated by the addition of
Variable Length Arrays, which allow the bound to be a
runtime expression in some cases and unspecified in others,
but still "If the expression is a constant expression,
it shall have a value greater than zero."

Unfortunately some compilers, notably gcc, support
bound-0 arrays as an extension, so to work there use:
  char dummy[ (boolexpr)*2-1 ];
which is strictly negative if the expression is false (0)
and a diagnosed error on every compiler I've ever seen.
If boolexpr is only nonzero/0 rather than the canonical 1/0,
and thus might overflow, do:
  char dummy[ ((expr)!=0)*2-1 ];
or in either case if you prefer:
  char dummy[ expr ? +1 : -1 ];

--
- David.Thompson 1 now at worldnet.att.net