--- ai12s/ai12-0321-1.txt 2019/03/15 05:39:29 1.5 +++ ai12s/ai12-0321-1.txt 2019/04/06 05:08:50 1.6 @@ -753,3 +753,271 @@ **************************************************************** +From: Brad Moore +Sent: Sunday, March 17, 2019 10:56 AM + +>> +>> > pragma Assert((for some I in 1..T'Size => T'Modulus = 2**I)); +>> +>> For "type T is mod 1;", T'Size = 0, 2**T'Size = 1, and T'Modulus = 1. +>> +>> ;-) +> +> Tucker noted that it isn't a very good assertion, since someone could +> declare: +> +> type Biggie is mod 256 with Atomic, Size => 16; +> +> OTOH, we could decide to explicitly not care about such corner cases. + +Given the choice in this case, I think it's probably better to have an +assertion that always works, rather than one that mostly works, even if it +is a bit more expensive. +At least the assertion if enabled is only applied during generic instantiation. + +To address Bob's comment, it doesn't make sense to have bitwise operations on +a type that doesn't have any bits, so I would extend the assertion to; + +pragma Assert(T'Modulus > 1 and (for some I in 1..T'Size => T'Modulus = 2**I)); + + +In this case, it's too bad that Ada hadn't defined a nand keyword similar to +xor which could be used for logical or bitwise operations. +That could be used to get the ones complement of any modular type. Currently, +we have the "not" keyword, but that only gives you a ones complement if the +modulus of the type is binary. + +If we had that, then we could write instead; + +pragma Assert((T'Last nand T'Last) = 0); + +>> Note to Brad: Unlike signed integers, the base range of a modular +>> type is widened beyond the first subtype. +> +> Every time I read this, I'm confused. I even went and looked it up in +> the RM to be sure. I think there is a "not" missing somewhere. Perhaps you meant: +> +> Note to Brad: Unlike signed integers, the base range of a +> modular type is NOT widened beyond the first subtype. + +Bob later clarified that he had meant to put the NOT in. + +**************************************************************** + +From: Randy Brukardt +Sent: Monday, March 18, 2019 10:19 PM + +> To address Bob's comment, it doesn't make sense to have bitwise +> operations on a type that doesn't have any bits, so I would extend the +> assertion to; +> +> pragma Assert(T'Modulus > 1 and (for some I in 1..T'Size => T'Modulus +> = 2**I)); + +You probably need to guard against overflow when +T'Modulus = System.Max_Binary_Modulus, which is probably bigger than +root_integer'Last (which is a signed integer type). And this will be +evaluated using root_integer, since it is a universal_integer expression +that isn't static. + +Moreover, you don't need the pretest, since the quantified expression doesn't +allow T'Modulus = 1 (2**1 being 2, last I checked :-). Ergo: + +pragma Assert(T'Modulus = System.Max_Binary_Modulus or else + (for some I in 1..T'Size => T'Modulus = 2**I); + +As written, this will still overflow on a machine with a 32-bit root_integer +for something like: + type Funny is mod 7 with Atomic, Size => 32; +but this is truly weird, and the assertion would fail anyway for Funny -- not +sure it's worth ensuring a particular exception in this case (that is, +Assertion_Error vs. Constraint_Error). + +[And of course, change 32 to whatever the size of root_integer is, this will +fail on any machine unless it doesn't support maximum integer-sized atomics +-- which seems unlikely.] + +... +> If we had that, then we could write instead; +> +> pragma Assert((T'Last nand T'Last) = 0); + +Tricky! We probably want the assertion to be understandable to the relatively +causal reader, and this is not that. (Otherwise, we'd have to repeat it in +English so people know what they're allowed to do, which defeats the point.) + +**************************************************************** + +From: Tucker Taft +Sent: Tuesday, March 19, 2019 3:59 AM + +In any case, I would separate this from the arithmetic operations, and probably +put it in a separate AI, that I at least would suggest deferring for now. + +**************************************************************** + +From: Brad Moore +Sent: Friday, March 22, 2019 12:25 AM + +>> To address Bob's comment, it doesn't make sense to have bitwise +>> operations on a type that doesn't have any bits, so I would extend +>> the assertion to; +>> +>> pragma Assert(T'Modulus > 1 and (for some I in 1..T'Size => T'Modulus +>> = 2**I)); +> +> You probably need to guard against overflow when T'Modulus = +> System.Max_Binary_Modulus, which is probably bigger than +> root_integer'Last (which is a signed integer type). And this will be +> evaluated using root_integer, since it is a universal_integer expression +> that isn't static. + +Right, but what I had to do to get this to work involved jumping through a +rather extraordinary number of hoops. See below.... + +> Moreover, you don't need the pretest, since the quantified expression +> doesn't allow T'Modulus = 1 (2**1 being 2, last I checked :-). + +Right. + + Ergo: +> +> pragma Assert(T'Modulus = System.Max_Binary_Modulus or else +> (for some I in 1..T'Size => T'Modulus = 2**I); +> +> As written, this will still overflow on a machine with a 32-bit +> root_integer for something like: +> type Funny is mod 7 with Atomic, Size => 32; but this is truly +> weird, and the assertion would fail anyway for Funny -- not sure it's +> worth ensuring a particular exception in this case (that is, +> Assertion_Error vs. Constraint_Error). +> +> [And of course, change 32 to whatever the size of root_integer is, +> this will fail on any machine unless it doesn't support maximum +> integer-sized atomics which seems unlikely.] + +This works ordinarily, but doesn't work for a generic formal modular type. +Or at least it doesn't in GNAT. + +I get the following warnings for the compilation if I prepend the expression + Atomic_Type'Modulus = System.Max_Binary_Modulus or else + +atomic_operations-bitwise.ads:9:47: warning: non-static universal integer value out of range +atomic_operations-bitwise.ads:9:47: warning: "Constraint_Error" will be raised at run time + +This makes sense to me, as the generic doesn't know that its actual type wont +have a non-binary modulus. I suspect an assume-the-worst rule is being applied +here. The limit for a non-binary modulus as defined in +System.Max_Nonbinary_Modulus on GNAT is 2 ** Integer'Size - 1, which is much +smaller than System.Max_Binary_Modulus which is based on the size of a 64 bit +integer. + +More below.... + +> ... +>> If we had that, then we could write instead; +>> +>> pragma Assert((T'Last nand T'Last) = 0); +> +> Tricky! We probably want the assertion to be understandable to the +> relatively causal reader, and this is not that. (Otherwise, we'd have +> to repeat it in English so people know what they're allowed to do, +> which defeats the point.) + +I think either assertion is likely to cause some head-scratching for the casual +reader (or even a causal reader ;-) ). + +I think a better solution is to define a boolean expression function whose +name describes the property, then the body of the expression function can +be more esoteric, tricky, or super-complicated, as it seems we need to do +in current Ada. The name of the function documents the intent. + +e.g + +generic + type Atomic_Type is mod <> with Atomic; +package Atomic_Operations.Bitwise with Pure, Nonblocking is + + function Atomic_Type_Has_Binary_Modulus return Boolean is + ((T'Last nand T'Last) = 0) + + pragma Assert (Atomic_Type_Has_Binary_Modulus); + + +Note, to have the Assert call a function of the package, it needs to be an +expression function, otherwise you get a Program_Error due to elaboration +problems. + +So suppose we wanted to write this assertion using current Ada, without +adding a nand keyword to the language. + +This ended up being a real struggle for me, but this is what I ended up with, +that seems to work. This seems to handle any modular type, as well as any +combination of 'Size aspect applied to the type. (I think, although there may +be some cases that dont work. The ones I tried seem to work at least). + +generic + type Atomic_Type is mod <> with Atomic; +package Atomic_Operations.Bitwise with Pure, Nonblocking is + + function Atomic_Type_Has_Binary_Modulus return Boolean is + (Atomic_Type'Mod (2) = 0 or else + (for all I in 1 .. Atomic_Type'Size - 1 => + (for some K in 1 .. I - 1 => + 2 * Atomic_Type (2**(K - 1)) < Atomic_Type (2**(K - 1))) + or else + (Atomic_Type'Last and 2 * Atomic_Type (2**(I - 1))) = 0 + or else + (for all J in 0 .. I - 1 => + (Atomic_Type'Last and Atomic_Type (2**J)) /= 0))); + + + pragma Assert (Atomic_Type_Has_Binary_Modulus); + +... + + +I gave up on trying to use 'Modulus. Randy's suggestion worked for non-generic +code, but when you try to use this attributes in a generic, I found it too +hard to compare the attribute result to test for overflow. + +This is because 'Modulus result is a universal integer, which is non-static in +the generic specification, so you cant compare it to System.Max_Binary_Modulus. + +Similarly, the argument for the 'Mod attribute is a universal integer, so you +have to be careful to not pass in a value that is too large. I also ran into +trouble using the expression 2**I, because that the type of I is natural, and +so 2**I is an integer expression, which can overflow. So I had to write +2**(I-1), then convert that to the atomic type, and then multiply by 2 to get +the modular value that I really wanted to work with. That multiplication by 2 +is a modular operation (that can wrap around) + +The approach is to keep testing higher bits, and if a 1 is found, then check +all lower bits to see if there are any zeroes. +If a zero bit is found, just ignore it and keep searching. + +The way I dealt with overflow is handled in the first part of the expression +function, where I test all previous iterations to see if the modular type +wrapped around. If a wrap around was found then we know we've already got the +answer, and just let the remaining iterations finish without checking the else +clauses. + +I must admit, this is a pretty complicated function to just check a modular +type to see if the modulus is a power two! There may be a simpler solution, +but every idea I came up with kept hitting roadblocks. + +It would sure be nice to have some sort of nand capability or similar, to make +writing such contracts simpler and easier to write. + +If not for Ada202x, then hopefully a next one after that. + +But at least it seems there is a way to do it in current Ada, but its not +pretty. + +Alternatively, we could do away with the assertion, and just document that +an instance of the generic will raise an exception if the Modular formal type +has a modulus that is not a power of two. But it seems that in Ada 202x, one +ought to have visible contracts for such an assertion. + +**************************************************************** +

Questions? Ask the ACAA Technical Agent