Regression

CodeHawk/CHC/cchanalyze/cCHPOQuery.ml

@@ -46,6 +46,7 @@ open Xsimplify
 open XprUtil
 
 (* cchlib *)
+open CCHArithmeticConversion
 open CCHBasicTypes
 open CCHExternalPredicate
 open CCHFileContract
@@ -1685,24 +1686,32 @@ object (self)
                 ~ok:(fun ty1 ->
                   TR.tfold
                     ~ok:(fun ty2 ->
-                      begin
-                        match op with
-                        | XPlus ->
-                           Some (BinOp (PlusA, a1, a2, get_integer_promotion ty1 ty2))
-                        | XMinus ->
-                           Some (BinOp (MinusA, a1, a2, get_integer_promotion ty1 ty2))
-                        | XMult ->
-                           Some (BinOp (Mult, a1, a2, get_integer_promotion ty1 ty2))
-                        | XDiv ->
-                           Some (BinOp (Div, a1, a2, get_integer_promotion ty1 ty2))
-                        | XShiftrt -> Some (BinOp (Shiftrt, a1, a2, ty1))
-                        | XShiftlt -> Some (BinOp (Shiftlt, a1, a2, ty1))
-                        | XLt -> Some (BinOp (Lt, a1, a2, TInt (IBool,[])))
-                        | XLe -> Some (BinOp (Le, a1, a2, TInt (IBool,[])))
-                        | XGt -> Some (BinOp (Gt, a1, a2, TInt (IBool,[])))
-                        | XGe -> Some (BinOp (Ge, a1, a2, TInt (IBool,[])))
-                        | _ -> None
-                      end)
+                      TR.tfold
+                         ~ok:(fun resulttyp ->
+                           begin
+                             match op with
+                             | XPlus -> Some (BinOp (PlusA, a1, a2, resulttyp))
+                             | XMinus -> Some (BinOp (MinusA, a1, a2, resulttyp))
+                             | XMult -> Some (BinOp (Mult, a1, a2, resulttyp))
+                             | XDiv -> Some (BinOp (Div, a1, a2, resulttyp))
+                             | XShiftrt -> Some (BinOp (Shiftrt, a1, a2, ty1))
+                             | XShiftlt -> Some (BinOp (Shiftlt, a1, a2, ty1))
+                             | XLt -> Some (BinOp (Lt, a1, a2, TInt (IBool, [])))
+                             | XLe -> Some (BinOp (Le, a1, a2, TInt (IBool, [])))
+                             | XGt -> Some (BinOp (Gt, a1, a2, TInt (IBool, [])))
+                             | XGe -> Some (BinOp (Ge, a1, a2, TInt (IBool, [])))
+                             | _ -> None
+                           end)
+                         ~error:(fun err ->
+                           begin
+                             log_diagnostics_result
+                               ~tag:"x2api:integer-promotion"
+                               ~msg:self#env#get_functionname
+                               __FILE__ __LINE__
+                               [String.concat ", " err];
+                             None
+                           end)
+                         (usual_arithmetic_conversion ty1 ty2))
                     ~error:(fun err ->
                       begin
                         log_diagnostics_result

CodeHawk/CHC/cchcil/cCHXParseFile.ml

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020-2021 Henny B. Sipma
-   Copyright (c) 2022-2024 Aarno Labs LLC
+   Copyright (c) 2022-2026 Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
    of this software and associated documentation files (the "Software"), to deal
@@ -72,6 +72,8 @@ let speclist = [
      "directory to store the generated xml files");
     ("-keep_system_includes", Arg.Unit (fun () -> keep_system_includes := true),
      "don't filter out functions in files with an absolute path name");
+    ("-loglevel", Arg.String set_log_level,
+     "set level for logging (default: WARNING)");
     ("-keepUnused",
      Arg.Set keepUnused, "keep unused type and function definitions")]
 
@@ -263,7 +265,6 @@ let save_xml_file f =
 let main () =
   try
     let _ = read_args () in
-    let _ = set_log_level "DEBUG" in
     let _ = cildeclarations#set_filename !filename in
     let cilfile = Frontc.parse !filename () in
     let _ = log_info "Parsed %s [%s:%d]" !filename __FILE__ __LINE__ in

CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml

@@ -135,6 +135,8 @@ let speclist = [
    "disable printing timing log messages");
   ("-verbose", Arg.Unit (fun () -> system_settings#set_verbose true),
    "print status on proof obligations and invariants");
+  ("-loglevel", Arg.String set_log_level,
+   "set level for logging (default: WARNING)");
   ("-projectname", Arg.String system_settings#set_projectname,
    "name of the project (determines name of results directory)");
   ("-keep_system_includes",
@@ -166,7 +168,6 @@ let save_log_files (contenttype:string) =
 
 let main () =
   try
-    let _ = set_log_level "WARNING" in
     let _ = read_args () in
     let _ = chlog#set_max_entry_size 1000 in
     let _ = log_info "AIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAI" in

CodeHawk/CHC/cchlib/Makefile

@@ -46,6 +46,7 @@ MLIS := \
 	cCHCodewalker \
 	cCHTypesSize \
 	cCHTypesUtil \
+	cCHArithmeticConversion \
 	cCHBasicTypesXml \
 	cCHInterfaceDictionary \
 	cCHExternalPredicate \
@@ -74,6 +75,7 @@ SOURCES := \
 	cCHCodewalker \
 	cCHTypesSize \
 	cCHTypesUtil \
+	cCHArithmeticConversion \
 	cCHBasicTypesXml \
 	cCHInterfaceDictionary \
 	cCHExternalPredicate \

CodeHawk/CHC/cchlib/cCHArithmeticConversion.ml

@@ -0,0 +1,128 @@
+(* =============================================================================
+   CodeHawk C Analyzer
+   Author: Henny Sipma
+   ------------------------------------------------------------------------------
+   The MIT License (MIT)
+
+   Copyright (c) 2005-2019 Kestrel Technology LLC
+   Copyright (c) 2020-2024 Henny B. Sipma
+   Copyright (c) 2024-2026 Aarno Labs LLC
+
+   Permission is hereby granted, free of charge, to any person obtaining a copy
+   of this software and associated documentation files (the "Software"), to deal
+   in the Software without restriction, including without limitation the rights
+   to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+   copies of the Software, and to permit persons to whom the Software is
+   furnished to do so, subject to the following conditions:
+
+   The above copyright notice and this permission notice shall be included in all
+   copies or substantial portions of the Software.
+
+   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+   OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+   SOFTWARE.
+   ============================================================================= *)
+
+(* chutil *)
+open CHLogger
+open CHTraceResult
+
+(* cchlib *)
+open CCHBasicTypes
+open CCHTypesToPretty
+open CCHUtilities
+
+
+let p2s = CHPrettyUtil.pretty_to_string
+
+let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line)
+let elocm (line: int): string = (eloc line) ^ ": "
+
+
+let get_integer_promotion (ty: typ): typ =
+  let promote_ikind (ik: ikind): ikind =
+    match ik with
+    | IChar | ISChar | IUChar | IShort | IBool -> IInt
+    | IUShort -> IUInt
+    | _ -> ik in
+
+  match ty with
+  | TInt (ik, _) -> TInt (promote_ikind ik, [])
+  | TEnum (ename, _) ->
+     let einfo = CCHFileEnvironment.file_environment#get_enum ename in
+     TInt (promote_ikind einfo.ekind, [])
+  | _ ->
+     let _ =
+       log_diagnostics_result
+         ~tag:"get_integer_promotion: unexpected type"
+         __FILE__ __LINE__
+         [p2s (typ_to_pretty ty)] in
+     ty
+
+
+let usual_arithmetic_conversion (ty1: typ) (ty2: typ): typ traceresult =
+
+  let convert_float (fk1: fkind) (fk2: fkind): fkind =
+    let is_complex (fk: fkind) =
+      match fk with
+      | FComplexLongDouble | FComplexDouble | FComplexFloat -> true
+      | _ -> false in
+    match fk1, fk2 with
+    | FComplexLongDouble, _ -> FComplexLongDouble
+    | _, FComplexLongDouble -> FComplexLongDouble
+    | FComplexDouble, _ -> FComplexDouble
+    | _, FComplexDouble -> FComplexDouble
+    | FComplexFloat, _ -> FComplexFloat
+    | _, FComplexFloat -> FComplexFloat
+    | FLongDouble, other when is_complex other -> FComplexLongDouble
+    | other, FLongDouble when is_complex other -> FComplexLongDouble
+    | FLongDouble, _ | _, FLongDouble -> FLongDouble
+    | FDouble, other when is_complex other -> FComplexDouble
+    | other, FDouble when is_complex other -> FComplexDouble
+    | FDouble, _ | _, FDouble -> FDouble
+    | FFloat, FFloat -> FFloat in
+
+  let convert_int (ik1: ikind) (ik2: ikind): ikind =
+    match ik1, ik2 with
+    | IInt, ILong | ILong, IInt -> ILong
+    | IInt, ILongLong | ILongLong, IInt -> ILongLong
+    | ILong, ILongLong | ILongLong, ILong -> ILongLong
+    | IUInt, IULong | IULong, IUInt -> IULong
+    | _, IULongLong | IULongLong, _ -> IULongLong
+    | IInt, IUInt | IUInt, IInt -> IUInt
+    | ILong, IULong | IULong, ILong -> IULong
+    | IInt, IULong | IULong, IInt -> IULong
+    | ILong, IUInt | IUInt, ILong -> ILong
+    | ILongLong, IUInt | IUInt, ILongLong -> ILongLong
+    | IUInt128, _ | _, IUInt128 -> IUInt128
+    | IInt128, _ | _, IInt128 -> IInt128
+    | _ ->
+       (* this should not happen *)
+       raise
+         (CCHFailure
+            (LBLOCK [
+                 STR "Missing case in integer promotion: ";
+                 STR (int_type_to_string ik1);
+                 STR " and ";
+                 STR (int_type_to_string ik2)])) in                 
+
+  match ty1, ty2 with
+  | TFloat (fk1, _), TFloat (fk2, _) -> Ok (TFloat (convert_float fk1 fk2, []))
+  | TFloat _, _ -> Ok ty1
+  | _, TFloat _ -> Ok ty2
+  | _ ->
+     let pty1 = get_integer_promotion ty1 in
+     let pty2 = get_integer_promotion ty2 in
+     match pty1, pty2 with
+     | TInt (ik1, _), TInt (ik2, _) when ik1 = ik2 -> Ok (TInt (ik1, []))
+     | TInt (ik1, _), TInt (ik2, _) -> Ok (TInt (convert_int ik1 ik2, []))
+     | _ ->
+        Error [(elocm __LINE__)
+               ^ "not an arithmetic type: "
+               ^ (p2s (typ_to_pretty ty1))
+               ^ " or "
+               ^ (p2s (typ_to_pretty ty2))]

CodeHawk/CHC/cchlib/cCHArithmeticConversion.mli

@@ -0,0 +1,113 @@
+(* =============================================================================
+   CodeHawk C Analyzer
+   Author: Henny Sipma
+   ------------------------------------------------------------------------------
+   The MIT License (MIT)
+
+   Copyright (c) 2005-2019 Kestrel Technology LLC
+   Copyright (c) 2020-2024 Henny B. Sipma
+   Copyright (c) 2024-2026 Aarno Labs LLC
+
+   Permission is hereby granted, free of charge, to any person obtaining a copy
+   of this software and associated documentation files (the "Software"), to deal
+   in the Software without restriction, including without limitation the rights
+   to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+   copies of the Software, and to permit persons to whom the Software is
+   furnished to do so, subject to the following conditions:
+
+   The above copyright notice and this permission notice shall be included in all
+   copies or substantial portions of the Software.
+
+   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+   OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+   SOFTWARE.
+   ============================================================================= *)
+
+(* chutil *)
+open CHTraceResult
+
+(* cchlib *)
+open CCHBasicTypes
+
+(** The Usual Arithmetic Conversions (C Standard 6.3.1.8)
+
+    All of the usual arithmetic conversions applied to expressions in the C
+    source code are supplied by the CIL parser in the form of casts.
+
+    The implementation in this file serves to determine the result type of an
+    expression constructed to serve as a precondition or side effect to a
+    function.
+ *)
+
+
+(** {1 Integer promotion: C Standard 6.3.1.1}
+
+    The following may be used in an expression wherever an int or unsigned
+    int may be used:
+    - an object or expression with an integer type whose integer conversion
+    rank is less than or equal to the rank of int and unsigned int.
+    - a bit-field of type _Bool, int, signed int, unsigned int.
+
+    If an int can represent all values of the original type, the value is
+    converted to an int; otherwise it is converted to an unsigned int. These
+    are called the integer promotions. All other types are unchanged by the
+    integer promotions.
+
+    The integer promotions preserve value including sign.
+ *)
+
+val get_integer_promotion: typ -> typ
+
+
+(** {1 Usual arithmetic conversions: C Standard 6.3.1.8}
+
+    Many operators that expect operands of arithmetic type cause conversions
+    and yield result types in a similar way. The purpose is to determine a
+    common real type for the operands and result. For the specified operands,
+    each operand is converted, without change of type domain, to a type whose
+    corresponding real type is the common real type. Unless explicitly stated
+    otherwise, the common real type is also the corresponding real type of
+    the result, whose type domain is the type domain of the operands if they
+    are the same, and complex otherwise. This pattern is called 'the usual
+    arithmetic conversions'.
+
+    First, if the corresponding real type of either operand is long double,
+    the other operand is converted, without change of type domain, to a type
+    whose corresponding real type is long double.
+
+    Otherwise, if the corresponding real type of either operand is double, the
+    other operand is converted, without change of type domain, to a type
+    whose corresponding real type is double.
+
+    Otherwise, if the corresponding real type of either operand is float, the
+    other operand is converted, without change of type domain, to a type whose
+    corresponding type is float.
+
+    Other, the integer promotions are performed on both operands. Then the
+    following rules are applied to the promoted operands:
+
+    If both operands have the same type, then no further conversion is needed.
+
+    Otherwise, if both operands have signed integer types or both have unsigned
+    integer types, the operand with the type of lesser integer conversion rank
+    is converted to the type of the operand with greater rank.
+
+    Otherwise, if the operand that has unsigned integer type has rank greater
+    or equal to the rank of the type of the other operand, then the operand
+    with signed integer type is converted to the type of the operand with
+    unsigned integer type.
+
+    Otherwise, if the type of the operand with signed integer type can represent
+    all of the values of the type of the operand with unsigned integer type, then
+    the operand with unsigned integer type is converted to the type of the operand
+    with signed integer type.
+
+    Otherwise, both operands are converted to the unsigned integer type
+    corresponding  to the type of the operand with signed integer type.
+ *)
+
+val usual_arithmetic_conversion: typ -> typ -> typ traceresult