Merge pull request #985 from goblint/float128

Support for machines where `float128` is not the same size as `long double`

Author: michael-schwarz

goblint.opam

@@ -74,7 +74,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#c03ade107208546ef59cd14dcefa7b55f1506494" ]
+  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4ef5a0865ce81c740c93da73e20a4f26daab3f1b" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # TODO: add back after release, only pinned for CI stability

goblint.opam.locked

@@ -128,7 +128,7 @@ conflicts: [
 pin-depends: [
   [
     "goblint-cil.2.0.1"
-    "git+https://github.com/goblint/cil.git#c03ade107208546ef59cd14dcefa7b55f1506494"
+    "git+https://github.com/goblint/cil.git#4ef5a0865ce81c740c93da73e20a4f26daab3f1b"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#c03ade107208546ef59cd14dcefa7b55f1506494" ]
+  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4ef5a0865ce81c740c93da73e20a4f26daab3f1b" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # TODO: add back after release, only pinned for CI stability

src/analyses/base.ml

@@ -782,8 +782,8 @@ struct
       | Const (CInt (num,ikind,str)) ->
         (match str with Some x -> M.tracel "casto" "CInt (%s, %a, %s)\n" (Cilint.string_of_cilint num) d_ikind ikind x | None -> ());
         `Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))
-      | Const (CReal (_, (FFloat | FDouble | FLongDouble as fkind), Some str)) -> `Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *)
-      | Const (CReal (num, (FFloat | FDouble | FLongDouble as fkind), None)) -> `Float (FD.of_const fkind num)
+      | Const (CReal (_,fkind, Some str)) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *)
+      | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.of_const fkind num)
       (* String literals *)
       | Const (CStr (x,_)) -> `Address (AD.from_string x) (* normal 8-bit strings, type: char* *)
       | Const (CWStr (xs,_) as c) -> (* wide character strings, type: wchar_t* *)

src/cdomains/floatDomain.ml

@@ -784,38 +784,44 @@ module FloatIntervalImplLifted = struct
   type t =
     | F32 of F1.t
     | F64 of F2.t
-    | FLong of F2.t [@@deriving to_yojson, eq, ord, hash]
+    | FLong of F2.t
+    | FFloat128 of F2.t [@@deriving to_yojson, eq, ord, hash]
 
   let show = function
     | F32 a -> "float: " ^ F1.show a
     | F64 a -> "double: " ^ F2.show a
     | FLong a -> "long double: " ^ F2.show a
+    | FFloat128 a -> "float128: " ^ F2.show a
 
   let lift2 (op32, op64) x y = match x, y with
     | F32 a, F32 b -> F32 (op32 a b)
     | F64 a, F64 b -> F64 (op64 a b)
     | FLong a, FLong b -> FLong (op64 a b)
+    | FFloat128 a, FFloat128 b -> FFloat128 (op64 a b)
     | _ -> failwith ("fkinds do not match. Values: " ^ show x ^ " and " ^ show y)
 
   let lift2_cmp (op32, op64) x y = match x, y with
     | F32 a, F32 b -> op32 a b
     | F64 a, F64 b -> op64 a b
     | FLong a, FLong b -> op64 a b
+    | FFloat128 a, FFloat128 b -> op64 a b
     | _ -> failwith ("fkinds do not match. Values: " ^ show x ^ " and " ^ show y)
 
   let lift (op32, op64) = function
     | F32 a -> F32 (op32 a)
     | F64 a -> F64 (op64 a)
     | FLong a -> FLong (op64 a)
+    | FFloat128 a -> FFloat128 (op64 a)
 
   let dispatch (op32, op64) = function
     | F32 a -> op32 a
-    | F64 a | FLong a -> op64 a
+    | F64 a | FLong a  | FFloat128 a-> op64 a
 
   let dispatch_fkind fkind (op32, op64) = match fkind with
     | FFloat -> F32 (op32 ())
     | FDouble -> F64 (op64 ())
     | FLongDouble -> FLong (op64 ())
+    | FFloat128 -> FFloat128 (op64 ())
     | _ ->
       (* this should never be reached, as we have to check for invalid fkind elsewhere,
          however we could instead of crashing also return top_of some fkind to avoid this and nonetheless have no actual information about anything*)
@@ -869,6 +875,7 @@ module FloatIntervalImplLifted = struct
     | F32 _ -> FFloat
     | F64 _ -> FDouble
     | FLong _ -> FLongDouble
+    | FFloat128 _ -> FFloat128
 
   let leq = lift2_cmp (F1.leq, F2.leq)
   let join = lift2 (F1.join, F2.join)

src/cdomains/valueDomain.ml

@@ -144,7 +144,7 @@ struct
     match t with
     | t when is_mutex_type t -> `Mutex
     | TInt (ik,_) -> `Int (ID.top_of ik)
-    | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.top_of fkind)
+    | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.top_of fkind)
     | TPtr _ -> `Address AD.top_ptr
     | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> init_value ~varAttr:fd.fattr fd.ftype) ci)
     | TComp ({cstruct=false; _},_) -> `Union (Unions.top ())
@@ -161,7 +161,7 @@ struct
     match t with
     | _ when is_mutex_type t -> `Mutex
     | TInt (ik,_) -> `Int (ID.(cast_to ik (top_of ik)))
-    | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.top_of fkind)
+    | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.top_of fkind)
     | TPtr _ -> `Address AD.top_ptr
     | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> top_value ~varAttr:fd.fattr fd.ftype) ci)
     | TComp ({cstruct=false; _},_) -> `Union (Unions.top ())
@@ -191,7 +191,7 @@ struct
     match t with
     | _ when is_mutex_type t -> `Mutex
     | TInt (ikind, _) -> `Int (ID.of_int ikind BI.zero)
-    | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.of_const fkind 0.0)
+    | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> `Float (FD.of_const fkind 0.0)
     | TPtr _ -> `Address AD.null_ptr
     | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> zero_init_value ~varAttr:fd.fattr fd.ftype) ci)
     | TComp ({cstruct=false; _} as ci,_) ->
@@ -280,10 +280,13 @@ struct
     | TFloat (FDouble,_), TFloat (FFloat,_) -> true
     | TFloat (FLongDouble,_), TFloat (FFloat,_) -> true
     | TFloat (FLongDouble,_), TFloat (FDouble,_) -> true
+    | TFloat (FFloat128, _), TFloat (FFloat,_) -> true
+    | TFloat (FFloat128, _), TFloat (FDouble,_) -> true
+    | TFloat (FFloat128, _), TFloat (FLongDouble,_) -> true
     | _, TFloat _ -> false (* casting float to an integral type always looses the decimals *)
-    | TFloat ((FFloat | FDouble | FLongDouble), _), TInt((IBool | IChar | IUChar | ISChar | IShort | IUShort), _) -> true (* resonably small integers can be stored in all fkinds *)
-    | TFloat ((FDouble | FLongDouble), _), TInt((IInt | IUInt | ILong | IULong), _) -> true (* values stored in between 16 and 32 bits can only be stored in at least doubles *)
-    | TFloat _, _ -> false (* all wider integers can not be completly put into a float, partially because our internal representation of long double is the same as for doubles *)
+    | TFloat (fk, _), TInt((IBool | IChar | IUChar | ISChar | IShort | IUShort), _) when not (Cilfacade.isComplexFKind fk)  -> true (* reasonably small integers can be stored in all fkinds *)
+    | TFloat ((FDouble | FLongDouble | FFloat128), _), TInt((IInt | IUInt | ILong | IULong), _) -> true (* values stored in between 16 and 32 bits can only be stored in at least doubles *)
+    | TFloat _, _ -> false (* all wider integers can not be completely put into a float, partially because our internal representation of long double is the same as for doubles *)
     | (TInt _ | TEnum _ | TPtr _) , (TInt _ | TEnum _ | TPtr _) ->
       IntDomain.Size.is_cast_injective ~from_type:t1 ~to_type:t2 && bitsSizeOf t2 >= bitsSizeOf t1
     | _ -> false
@@ -388,7 +391,7 @@ struct
                 (match Structs.get x first with `Int x -> x | _ -> raise CastError)*)
               | _ -> log_top __POS__; ID.top_of ik
             ))
-        | TFloat ((FFloat | FDouble | FLongDouble as fkind),_) ->
+        | TFloat (fkind,_) when not (Cilfacade.isComplexFKind fkind) ->
           (match v with
            |`Int ix ->  `Float (FD.of_int fkind ix)
            |`Float fx ->  `Float (FD.cast_to fkind fx)
@@ -809,7 +812,7 @@ struct
                (* only return an actual value if we have a type and return actually the exact same type *)
                | `Float f_value, TFloat(fkind, _) when FD.get_fkind f_value = fkind -> `Float f_value
                | `Float _, t -> top_value t
-               | _, TFloat((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.top_of fkind)
+               | _, TFloat(fkind, _)  when not (Cilfacade.isComplexFKind fkind)-> `Float (FD.top_of fkind)
                | _ ->
                  let x = cast ~torg:l_fld.ftype fld.ftype value in
                  let l', o' = shift_one_over l o in

src/util/cilfacade.ml

@@ -201,13 +201,25 @@ let typeOfRealAndImagComponents t =
       | FFloat -> FFloat      (* [float] *)
       | FDouble -> FDouble     (* [double] *)
       | FLongDouble -> FLongDouble (* [long double] *)
+      | FFloat128 -> FFloat128 (* [float128] *)
       | FComplexFloat -> FFloat
       | FComplexDouble -> FDouble
       | FComplexLongDouble -> FLongDouble
+      | FComplexFloat128 -> FComplexFloat128
     in
     TFloat (newfkind fkind, attrs)
   | _ -> raise (TypeOfError RealImag_NonNumerical)
 
+let isComplexFKind = function
+  | FFloat
+  | FDouble
+  | FLongDouble
+  | FFloat128 -> false
+  | FComplexFloat
+  | FComplexDouble
+  | FComplexLongDouble
+  | FComplexFloat128 -> true
+
 let rec typeOf (e: exp) : typ =
   match e with
   | Const(CInt (_, ik, _)) -> TInt(ik, [])