[M3devel] [Fwd: Sanity check request regarding CT arithmetic]

[Rodney M. Bates]

Ah, and this is a systematic way of ensuring the precondition
a.n=b.n always holds.  Does the MIN function hint at someday
generalizing to not require this condition?  That would be tidy,
but seems like an awful lot of work, if it is never used.

Tony Hosking wrote:
> Hi Rodney,
> 
> Yes, you are missing one crucial thing.  Namely, that the front-end  
> compiler *carefully* uses these target integer simulations only with  
> values that are *explicitly* the same length.  LONGINT and INTEGER  are 
> different types.  INTEGER is the *representation* type for all  values 
> 32 bits or less.  LONGINT is the representation type for only  LONGINT 
> values.  You cannot mix LONGINT with INTEGER in source code  
> expressions.  They need to be converted explicitly using ORD/VAL.   
> Indeed, you are right that the interfaces should document that  behavior 
> explicitly, or alternatively, perhaps the implementations  should 
> <*ASSERT a.n=b.n*>.  The change from the way PM3 does things  was 
> necessary for the introduction of LONGINT.
> 
> Hope this helps and sorry for the imprecision of documentation.
> 
> On Jan 31, 2008, at 11:22 AM, Rodney M. Bates wrote:
> 
>> Whenever I run across something this unbelievable, I figure I must
>> be missing something.  Can anybody tell me what?
>>
>> While working on making Pickles work on LONGINT, I have noted the
>> following code snippets for doing target arithmetic at compile time:
>>
>> From m3-sys/m3middle/src/Target.i3:
>>
>> (* The bits of a target INTEGER (in 2's complement) are stored in
>>    an array of small host values, with the low order bits in the first
>>    element of the array. *)
>>
>> TYPE
>>   Int = (* OPAQUE *) RECORD
>>     n: CARDINAL;          (* only bytes [0..n-1] contain valid bits *)
>>     x := IBytes{0,..};    (* default is Zero *)
>>   END;
>>   IBytes = ARRAY [0..7] OF IByte;
>>   IByte = BITS 8 FOR [0..16_ff];
>>
>> From m3-sys/m3middle/src/TWord.m3:
>>
>> PROCEDURE Subtract (READONLY a, b: Int;  VAR r: Int) =
>>   VAR borrow := 0;  n := MIN (a.n, b.n);
>>   BEGIN
>>     <*ASSERT n # 0*>
>>     r.n := n;
>>     FOR i := 0 TO n-1 DO
>>       borrow := a.x[i] - b.x[i] - borrow;
>>       r.x[i] := Word.And (borrow, Mask);
>>       borrow := Word.And (RShift (borrow, BITSIZE (IByte)), 1);
>>     END;
>>   END Subtract;
>>
>> Unless the two values have equal numbers of bytes, Subtract just
>> throws away the high bytes of the longer operand.  It looks like
>> pretty much all the CT target arithmetic in TWord.m3 and TInt.m3
>> does this.
>>
>> It seems just about inconceivable that the arithmetic could be this
>> broken and not have created many impossible-to-ignore bugs.  SRC
>> and pm3 do it differently.  They have a single global variable that
>> gives the used size of all CT target values.
>>
>> The only possible explanation I can think of is that the cm3 compiler
>> happens never to pass two Target.Int values with different values  of n.
>> The relevant declarations give no hint of such a counter-intuitive
>> requirement.  If this is an essential precondition, it should be
>> documented in the interfaces.
>>
>> -- 
>> -------------------------------------------------------------
>> Rodney M. Bates, retired assistant professor
>> Dept. of Computer Science, Wichita State University
>> Wichita, KS 67260-0083
>> 316-978-3922
>> rodney.bates at wichita.edu
>>
>>
> 
> 

-- 
-------------------------------------------------------------
Rodney M. Bates, retired assistant professor
Dept. of Computer Science, Wichita State University
Wichita, KS 67260-0083
316-978-3922
rodney.bates at wichita.edu