Skip to content

Commit 31a03dc

Browse files
sipmasipma
committed
CHC: redo usual arithmetic conversions
1 parent b4e7f9e commit 31a03dc

7 files changed

Lines changed: 273 additions & 106 deletions

File tree

‎CodeHawk/CHC/cchanalyze/cCHPOQuery.ml‎

Lines changed: 27 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ open Xsimplify
4646
open XprUtil
4747

4848
(* cchlib *)
49+
open CCHArithmeticConversion
4950
open CCHBasicTypes
5051
open CCHExternalPredicate
5152
open CCHFileContract
@@ -1685,24 +1686,32 @@ object (self)
16851686
~ok:(fun ty1 ->
16861687
TR.tfold
16871688
~ok:(fun ty2 ->
1688-
begin
1689-
match op with
1690-
| XPlus ->
1691-
Some (BinOp (PlusA, a1, a2, get_integer_promotion ty1 ty2))
1692-
| XMinus ->
1693-
Some (BinOp (MinusA, a1, a2, get_integer_promotion ty1 ty2))
1694-
| XMult ->
1695-
Some (BinOp (Mult, a1, a2, get_integer_promotion ty1 ty2))
1696-
| XDiv ->
1697-
Some (BinOp (Div, a1, a2, get_integer_promotion ty1 ty2))
1698-
| XShiftrt -> Some (BinOp (Shiftrt, a1, a2, ty1))
1699-
| XShiftlt -> Some (BinOp (Shiftlt, a1, a2, ty1))
1700-
| XLt -> Some (BinOp (Lt, a1, a2, TInt (IBool,[])))
1701-
| XLe -> Some (BinOp (Le, a1, a2, TInt (IBool,[])))
1702-
| XGt -> Some (BinOp (Gt, a1, a2, TInt (IBool,[])))
1703-
| XGe -> Some (BinOp (Ge, a1, a2, TInt (IBool,[])))
1704-
| _ -> None
1705-
end)
1689+
TR.tfold
1690+
~ok:(fun resulttyp ->
1691+
begin
1692+
match op with
1693+
| XPlus -> Some (BinOp (PlusA, a1, a2, resulttyp))
1694+
| XMinus -> Some (BinOp (MinusA, a1, a2, resulttyp))
1695+
| XMult -> Some (BinOp (Mult, a1, a2, resulttyp))
1696+
| XDiv -> Some (BinOp (Div, a1, a2, resulttyp))
1697+
| XShiftrt -> Some (BinOp (Shiftrt, a1, a2, ty1))
1698+
| XShiftlt -> Some (BinOp (Shiftlt, a1, a2, ty1))
1699+
| XLt -> Some (BinOp (Lt, a1, a2, TInt (IBool, [])))
1700+
| XLe -> Some (BinOp (Le, a1, a2, TInt (IBool, [])))
1701+
| XGt -> Some (BinOp (Gt, a1, a2, TInt (IBool, [])))
1702+
| XGe -> Some (BinOp (Ge, a1, a2, TInt (IBool, [])))
1703+
| _ -> None
1704+
end)
1705+
~error:(fun err ->
1706+
begin
1707+
log_diagnostics_result
1708+
~tag:"x2api:integer-promotion"
1709+
~msg:self#env#get_functionname
1710+
__FILE__ __LINE__
1711+
[String.concat ", " err];
1712+
None
1713+
end)
1714+
(usual_arithmetic_conversion ty1 ty2))
17061715
~error:(fun err ->
17071716
begin
17081717
log_diagnostics_result

‎CodeHawk/CHC/cchlib/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ MLIS := \
4646
cCHCodewalker \
4747
cCHTypesSize \
4848
cCHTypesUtil \
49+
cCHArithmeticConversion \
4950
cCHBasicTypesXml \
5051
cCHInterfaceDictionary \
5152
cCHExternalPredicate \
@@ -74,6 +75,7 @@ SOURCES := \
7475
cCHCodewalker \
7576
cCHTypesSize \
7677
cCHTypesUtil \
78+
cCHArithmeticConversion \
7779
cCHBasicTypesXml \
7880
cCHInterfaceDictionary \
7981
cCHExternalPredicate \

‎CodeHawk/CHC/cchlib/cCHArithmeticConversion.ml‎

Lines changed: 128 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,128 @@
1+
(* =============================================================================
2+
CodeHawk C Analyzer
3+
Author: Henny Sipma
4+
------------------------------------------------------------------------------
5+
The MIT License (MIT)
6+
7+
Copyright (c) 2005-2019 Kestrel Technology LLC
8+
Copyright (c) 2020-2024 Henny B. Sipma
9+
Copyright (c) 2024-2026 Aarno Labs LLC
10+
11+
Permission is hereby granted, free of charge, to any person obtaining a copy
12+
of this software and associated documentation files (the "Software"), to deal
13+
in the Software without restriction, including without limitation the rights
14+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
15+
copies of the Software, and to permit persons to whom the Software is
16+
furnished to do so, subject to the following conditions:
17+
18+
The above copyright notice and this permission notice shall be included in all
19+
copies or substantial portions of the Software.
20+
21+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
22+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
23+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
24+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
25+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
26+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
27+
SOFTWARE.
28+
============================================================================= *)
29+
30+
(* chutil *)
31+
open CHLogger
32+
open CHTraceResult
33+
34+
(* cchlib *)
35+
open CCHBasicTypes
36+
open CCHTypesToPretty
37+
open CCHUtilities
38+
39+
40+
let p2s = CHPrettyUtil.pretty_to_string
41+
42+
let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line)
43+
let elocm (line: int): string = (eloc line) ^ ": "
44+
45+
46+
let get_integer_promotion (ty: typ): typ =
47+
let promote_ikind (ik: ikind): ikind =
48+
match ik with
49+
| IChar | ISChar | IUChar | IShort | IBool -> IInt
50+
| IUShort -> IUInt
51+
| _ -> ik in
52+
53+
match ty with
54+
| TInt (ik, _) -> TInt (promote_ikind ik, [])
55+
| TEnum (ename, _) ->
56+
let einfo = CCHFileEnvironment.file_environment#get_enum ename in
57+
TInt (promote_ikind einfo.ekind, [])
58+
| _ ->
59+
let _ =
60+
log_diagnostics_result
61+
~tag:"get_integer_promotion: unexpected type"
62+
__FILE__ __LINE__
63+
[p2s (typ_to_pretty ty)] in
64+
ty
65+
66+
67+
let usual_arithmetic_conversion (ty1: typ) (ty2: typ): typ traceresult =
68+
69+
let convert_float (fk1: fkind) (fk2: fkind): fkind =
70+
let is_complex (fk: fkind) =
71+
match fk with
72+
| FComplexLongDouble | FComplexDouble | FComplexFloat -> true
73+
| _ -> false in
74+
match fk1, fk2 with
75+
| FComplexLongDouble, _ -> FComplexLongDouble
76+
| _, FComplexLongDouble -> FComplexLongDouble
77+
| FComplexDouble, _ -> FComplexDouble
78+
| _, FComplexDouble -> FComplexDouble
79+
| FComplexFloat, _ -> FComplexFloat
80+
| _, FComplexFloat -> FComplexFloat
81+
| FLongDouble, other when is_complex other -> FComplexLongDouble
82+
| other, FLongDouble when is_complex other -> FComplexLongDouble
83+
| FLongDouble, _ | _, FLongDouble -> FLongDouble
84+
| FDouble, other when is_complex other -> FComplexDouble
85+
| other, FDouble when is_complex other -> FComplexDouble
86+
| FDouble, _ | _, FDouble -> FDouble
87+
| FFloat, FFloat -> FFloat in
88+
89+
let convert_int (ik1: ikind) (ik2: ikind): ikind =
90+
match ik1, ik2 with
91+
| IInt, ILong | ILong, IInt -> ILong
92+
| IInt, ILongLong | ILongLong, IInt -> ILongLong
93+
| ILong, ILongLong | ILongLong, ILong -> ILongLong
94+
| IUInt, IULong | IULong, IUInt -> IULong
95+
| _, IULongLong | IULongLong, _ -> IULongLong
96+
| IInt, IUInt | IUInt, IInt -> IUInt
97+
| ILong, IULong | IULong, ILong -> IULong
98+
| IInt, IULong | IULong, IInt -> IULong
99+
| ILong, IUInt | IUInt, ILong -> ILong
100+
| ILongLong, IUInt | IUInt, ILongLong -> ILongLong
101+
| IUInt128, _ | _, IUInt128 -> IUInt128
102+
| IInt128, _ | _, IInt128 -> IInt128
103+
| _ ->
104+
(* this should not happen *)
105+
raise
106+
(CCHFailure
107+
(LBLOCK [
108+
STR "Missing case in integer promotion: ";
109+
STR (int_type_to_string ik1);
110+
STR " and ";
111+
STR (int_type_to_string ik2)])) in
112+
113+
match ty1, ty2 with
114+
| TFloat (fk1, _), TFloat (fk2, _) -> Ok (TFloat (convert_float fk1 fk2, []))
115+
| TFloat _, _ -> Ok ty1
116+
| _, TFloat _ -> Ok ty2
117+
| _ ->
118+
let pty1 = get_integer_promotion ty1 in
119+
let pty2 = get_integer_promotion ty2 in
120+
match pty1, pty2 with
121+
| TInt (ik1, _), TInt (ik2, _) when ik1 = ik2 -> Ok (TInt (ik1, []))
122+
| TInt (ik1, _), TInt (ik2, _) -> Ok (TInt (convert_int ik1 ik2, []))
123+
| _ ->
124+
Error [(elocm __LINE__)
125+
^ "not an arithmetic type: "
126+
^ (p2s (typ_to_pretty ty1))
127+
^ " or "
128+
^ (p2s (typ_to_pretty ty2))]

‎CodeHawk/CHC/cchlib/cCHArithmeticConversion.mli‎

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
(* =============================================================================
2+
CodeHawk C Analyzer
3+
Author: Henny Sipma
4+
------------------------------------------------------------------------------
5+
The MIT License (MIT)
6+
7+
Copyright (c) 2005-2019 Kestrel Technology LLC
8+
Copyright (c) 2020-2024 Henny B. Sipma
9+
Copyright (c) 2024-2026 Aarno Labs LLC
10+
11+
Permission is hereby granted, free of charge, to any person obtaining a copy
12+
of this software and associated documentation files (the "Software"), to deal
13+
in the Software without restriction, including without limitation the rights
14+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
15+
copies of the Software, and to permit persons to whom the Software is
16+
furnished to do so, subject to the following conditions:
17+
18+
The above copyright notice and this permission notice shall be included in all
19+
copies or substantial portions of the Software.
20+
21+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
22+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
23+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
24+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
25+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
26+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
27+
SOFTWARE.
28+
============================================================================= *)
29+
30+
(* chutil *)
31+
open CHTraceResult
32+
33+
(* cchlib *)
34+
open CCHBasicTypes
35+
36+
(** The Usual Arithmetic Conversions (C Standard 6.3.1.8)
37+
38+
All of the usual arithmetic conversions applied to expressions in the C
39+
source code are supplied by the CIL parser in the form of casts.
40+
41+
The implementation in this file serves to determine the result type of an
42+
expression constructed to serve as a precondition or side effect to a
43+
function.
44+
*)
45+
46+
47+
(** {1 Integer promotion: C Standard 6.3.1.1}
48+
49+
The following may be used in an expression wherever an int or unsigned
50+
int may be used:
51+
- an object or expression with an integer type whose integer conversion
52+
rank is less than or equal to the rank of int and unsigned int.
53+
- a bit-field of type _Bool, int, signed int, unsigned int.
54+
55+
If an int can represent all values of the original type, the value is
56+
converted to an int; otherwise it is converted to an unsigned int. These
57+
are called the integer promotions. All other types are unchanged by the
58+
integer promotions.
59+
60+
The integer promotions preserve value including sign.
61+
*)
62+
63+
val get_integer_promotion: typ -> typ
64+
65+
66+
(** {1 Usual arithmetic conversions: C Standard 6.3.1.8}
67+
68+
Many operators that expect operands of arithmetic type cause conversions
69+
and yield result types in a similar way. The purpose is to determine a
70+
common real type for the operands and result. For the specified operands,
71+
each operand is converted, without change of type domain, to a type whose
72+
corresponding real type is the common real type. Unless explicitly stated
73+
otherwise, the common real type is also the corresponding real type of
74+
the result, whose type domain is the type domain of the operands if they
75+
are the same, and complex otherwise. This pattern is called 'the usual
76+
arithmetic conversions'.
77+
78+
First, if the corresponding real type of either operand is long double,
79+
the other operand is converted, without change of type domain, to a type
80+
whose corresponding real type is long double.
81+
82+
Otherwise, if the corresponding real type of either operand is double, the
83+
other operand is converted, without change of type domain, to a type
84+
whose corresponding real type is double.
85+
86+
Otherwise, if the corresponding real type of either operand is float, the
87+
other operand is converted, without change of type domain, to a type whose
88+
corresponding type is float.
89+
90+
Other, the integer promotions are performed on both operands. Then the
91+
following rules are applied to the promoted operands:
92+
93+
If both operands have the same type, then no further conversion is needed.
94+
95+
Otherwise, if both operands have signed integer types or both have unsigned
96+
integer types, the operand with the type of lesser integer conversion rank
97+
is converted to the type of the operand with greater rank.
98+
99+
Otherwise, if the operand that has unsigned integer type has rank greater
100+
or equal to the rank of the type of the other operand, then the operand
101+
with signed integer type is converted to the type of the operand with
102+
unsigned integer type.
103+
104+
Otherwise, if the type of the operand with signed integer type can represent
105+
all of the values of the type of the operand with unsigned integer type, then
106+
the operand with unsigned integer type is converted to the type of the operand
107+
with signed integer type.
108+
109+
Otherwise, both operands are converted to the unsigned integer type
110+
corresponding to the type of the operand with signed integer type.
111+
*)
112+
113+
val usual_arithmetic_conversion: typ -> typ -> typ traceresult

0 commit comments

Comments
 (0)