blob: b48f4e67824e550474176013eaf143b18bbb9046 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
Mixed-type integer comparison
=============================
This is tricky:
int8 i = ...
uint64 j = ...
int32 k = ...
if i + j < k
There are two problems here:
1. Mixing range (signedness and type) in the operands of the comparison
2. What is the target type of the operands?
I.e. how to compute `i+j`?
To point 1, there's a simple solution: Just check whether the operands
are out of value, leading to an always-true or always-false comparison.
E.g. a negative value is less than any value of an unsigned type.
Point 2 is trickier to solve.
2a) Use algebra to determine whether the comparison returns true.
But this can get really tricky, for example if multiplication
appears on both sides of the expression, leading to possibly
very large values. Or the expressions might be impossible to
simplify enough to compute algebraically.
2b) Require either side to have a clear type
(this is what LRL did).
2b) Require the programmer to specify a target type.
Syntax examples:
i + j <(uint64) k
i + j (uint64)< k
i + j uint64 < k
(i + j) as uint64 < k as uint64
uint64_less (i + j) k
|
