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

[Tony Hosking]

On Feb 1, 2008, at 9:33 AM, Rodney M. Bates wrote:

> 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?

Yes, that's the general idea.

>   That would be tidy,
> but seems like an awful lot of work, if it is never used.

Yeah, I played around with this a great deal and decided it wasn't  
worth the effort.

>
> 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