Merge pull request #1813 from goblint/float16

Add `_Float16` parsing support

Author: sim642

goblint.opam

@@ -101,8 +101,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  # published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b" ]
+  [ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#8e2212316ceda6911de2db716933bfb8c64a8585" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

goblint.opam.locked

@@ -66,7 +66,7 @@ depends: [
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.6"}
+  "goblint-cil" {= "2.0.7"}
   "hex" {= "1.5.0"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "1.0.1"}
@@ -142,8 +142,8 @@ post-messages: [
 ]
 pin-depends: [
   [
-    "goblint-cil.2.0.6"
-    "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b"
+    "goblint-cil.2.0.7"
+    "git+https://github.com/goblint/cil.git#8e2212316ceda6911de2db716933bfb8c64a8585"
   ]
   [
     "apron.v0.9.15"

goblint.opam.template

@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b" ]
+  [ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#8e2212316ceda6911de2db716933bfb8c64a8585" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

gobview

@@ -1002,10 +1002,15 @@ module FloatIntervalImplLifted = struct
     | FDouble -> F64 (op64 ())
     | FLongDouble -> FLong (op64 ())
     | FFloat128 -> FFloat128 (op64 ())
-    | _ ->
+    | FFloat16 -> failwith "fkind FFloat16 not supported"
+    | FComplexFloat
+    | FComplexDouble
+    | FComplexLongDouble
+    | FComplexFloat128
+    | FComplexFloat16 ->
       (* 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*)
-      failwith "unsupported fkind"
+      failwith "complex fkind not supported"
 
   let neg = lift (F1.neg, F2.neg)
   let fabs = lift (F1.fabs, F2.fabs)

src/cdomain/value/cdomains/floatDomain.ml

@@ -357,13 +357,18 @@ struct
     (*| TPtr _, t -> bitsSizeOf t <= bitsSizeOf !upointType
       | t, TPtr _ -> bitsSizeOf t >= bitsSizeOf !upointType*)
     | TFloat (fk1,_), TFloat (fk2,_) when fk1 = fk2 -> true
+    | TFloat (FFloat,_), TFloat (FFloat16,_) -> true
     | TFloat (FDouble,_), TFloat (FFloat,_) -> true
+    | TFloat (FDouble,_), TFloat (FFloat16,_) -> true
     | TFloat (FLongDouble,_), TFloat (FFloat,_) -> true
     | TFloat (FLongDouble,_), TFloat (FDouble,_) -> true
+    | TFloat (FLongDouble,_), TFloat (FFloat16,_) -> true
     | TFloat (FFloat128, _), TFloat (FFloat,_) -> true
     | TFloat (FFloat128, _), TFloat (FDouble,_) -> true
     | TFloat (FFloat128, _), TFloat (FLongDouble,_) -> true
+    | TFloat (FFloat128, _), TFloat (FFloat16,_) -> true
     | _, TFloat _ -> false (* casting float to an integral type always looses the decimals *)
+    | TFloat (FFloat16, _), (TInt((IBool | IChar | IUChar | ISChar), _) | TEnum ({ekind = IBool | IChar | IUChar | ISChar; _}, _)) -> true (* reasonably small integers can be stored in _Float16 *)
     | TFloat (fk, _), (TInt((IBool | IChar | IUChar | ISChar | IShort | IUShort), _) | TEnum ({ekind = 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), _) | TEnum ({ekind = 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 *)

src/cdomain/value/cdomains/valueDomain.ml

@@ -144,10 +144,12 @@ struct
     | FDouble
     | FLongDouble
     | FFloat128
+    | FFloat16
     | FComplexFloat
     | FComplexDouble
     | FComplexLongDouble
     | FComplexFloat128
+    | FComplexFloat16
   [@@deriving hash]
   (* Hashtbl.hash doesn't monomorphize, so derive instead. *)
 

src/common/util/cilType.ml

@@ -297,10 +297,12 @@ let typeOfRealAndImagComponents t =
       | FDouble -> FDouble     (* [double] *)
       | FLongDouble -> FLongDouble (* [long double] *)
       | FFloat128 -> FFloat128 (* [float128] *)
+      | FFloat16 -> FFloat16 (* [_Float16] *)
       | FComplexFloat -> FFloat
       | FComplexDouble -> FDouble
       | FComplexLongDouble -> FLongDouble
       | FComplexFloat128 -> FComplexFloat128
+      | FComplexFloat16 -> FComplexFloat16
     in
     TFloat (newfkind fkind, attrs)
   | _ -> raise (TypeOfError RealImag_NonNumerical)
@@ -309,11 +311,13 @@ let isComplexFKind = function
   | FFloat
   | FDouble
   | FLongDouble
-  | FFloat128 -> false
+  | FFloat128
+  | FFloat16 -> false
   | FComplexFloat
   | FComplexDouble
   | FComplexLongDouble
-  | FComplexFloat128 -> true
+  | FComplexFloat128
+  | FComplexFloat16 -> true
 
 (** @raise TypeOfError *)
 let rec typeOf (e: exp) : typ =