[m-rev.] for review: extend constant propagation to sized integer types

[Zoltan Somogyi]

2023-04-19 14:12 GMT+10:00 "Julien Fischer" <jfischer at opturion.com>:
>>     Add predicates to emulate the logical operations AND, OR, XOR and NOT.
>>     With these, the original code (in const_prop.m) did *not* work by
>>     doing the operation on arbitrary precision integers. I am not sure
>>     if that was a deliberate decision to avoid integer.m's logical operations,
>>     which I expect would not have been tested nearly as thoroughly
>>     as the arithmetic ops.
> 
> I'm fairly certain that they haven't been as extensively tested, but I don't
> think that's the reason. (Note that the initial version of const_prop.m was in
> 1997, which predates the addition of bitwise operations to the integer module
> by two years.)

Yes, but I didn't know whether *not updating the code in const_prop.m when
those ops were added to integer.m* was a deliberate decision or not.
 
>>     ZZZ Does anyone know the history here?
> 
> AND, OR XOR and NOT are never going to extend a value beyond what can be
> represented by its type;

The problem comes in defining what "its type" means when
- the operand is word sized, and
- the word sizes of the host and target machines differ.

A bitwise negation *can* extend a value in that case, which is a bug
that you fixed yourself. That fix (not applying const prop if the word sizes differ)
will still work. I am concerned about integer.m's bitwise ops screwing up
*before* restricting their results to the result type's number of bits.

the original version of const_prop did not use
> int_emu.m (which was added in 2015). The treatment of these bitwise operations
> is what const_prop.m has always done.

Yes, I know that is what const_prop has always done; that is why I continued
that approach, just extending it to other types. What I meant by my question was:
does anyone know the history of the bitwise ops in integer.m? Specifically, I would
like to know whether they have been tested enough to use them here.

>> +    % All of the {int,uint}{,8,16,32,64} modules define unary plus,
>> +    % unary minus, and bitwise negation. The other procedures below
>> +    % are defined only in int.m; this is checked by the predicates that
>> +    % emulate them.
> 
> None of the uint* modules provide unary plus and unary minus.

Thanks for catching that, and for the review. I will add a check for signed ints,
and update the comment.

Zoltan.