Merge pull request #1896 from goblint/overflow-cast-kind

Add cast kinds to integer overflow messages

Author: sim642

src/analyses/base.ml

@@ -167,7 +167,7 @@ struct
    * Abstract evaluation functions
    **************************************************************************)
 
-  let iDtoIdx x = ID.cast_to (Cilfacade.ptrdiff_ikind ()) x
+  let iDtoIdx x = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) x (* TODO: proper castkind *)
 
   let unop_ID = function
     | Neg  -> ID.neg
@@ -182,7 +182,7 @@ struct
 
   (* Evaluating Cil's unary operators. *)
   let evalunop op typ: value -> value = function
-    | Int v1 -> Int (ID.cast_to (Cilfacade.get_ikind typ) (unop_ID op v1))
+    | Int v1 -> Int (ID.cast_to ~kind:Internal (Cilfacade.get_ikind typ) (unop_ID op v1)) (* TODO: proper castkind *)
     | Float v -> unop_FD op v
     | Address a when op = LNot ->
       if AD.is_null a then
@@ -332,7 +332,7 @@ struct
       (* Pointer subtracted by a value (e-i) is very similar *)
       (* Cast n to the (signed) ptrdiff_ikind, then add the its negated value. *)
       | MinusPI ->
-        let n = ID.neg (ID.cast_to (Cilfacade.ptrdiff_ikind ()) n) in
+        let n = ID.neg (ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) n) in (* TODO: proper castkind *)
         Address (ad_concat_map (addToAddr n) p)
       | Mod -> Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*)
       | _ -> Address AD.top_ptr
@@ -342,11 +342,11 @@ struct
     (* For the integer values, we apply the int domain operator *)
     | Int v1, Int v2 ->
       let result_ik = Cilfacade.get_ikind t in
-      Int (ID.cast_to result_ik (binop_ID result_ik op v1 v2))
+      Int (ID.cast_to ~kind:Internal result_ik (binop_ID result_ik op v1 v2)) (* TODO: proper castkind *)
     (* For the float values, we apply the float domain operators *)
     | Float v1, Float v2 when is_int_returning_binop_FD op ->
       let result_ik = Cilfacade.get_ikind t in
-      Int (ID.cast_to result_ik (int_returning_binop_FD op v1 v2))
+      Int (ID.cast_to ~kind:Internal result_ik (int_returning_binop_FD op v1 v2)) (* TODO: proper castkind *)
     | Float v1, Float v2 -> Float (binop_FD (Cilfacade.get_fkind t) op v1 v2)
     (* For address +/- value, we try to do some elementary ptr arithmetic *)
     | Address p, Int n
@@ -528,7 +528,7 @@ struct
         | Int _ ->
           let at = AD.type_of addrs in
           if Cil.isArithmeticType at then
-            VD.cast at x
+            VD.cast ~kind:Internal at x (* TODO: proper castkind *)
           else
             x
         | _ -> x
@@ -928,12 +928,12 @@ struct
         let array_start = add_offset_varinfo array_ofs in
         Address (AD.map array_start (eval_lv ~man st lval))
       | CastE (_, t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
-      | CastE (_, t, exp) ->
+      | CastE (kind, t, exp) ->
         (let v = eval_rv ~man st exp in
          try
-           VD.cast ~torg:(Cilfacade.typeOf exp) t v
+           VD.cast ~kind ~torg:(Cilfacade.typeOf exp) t v
          with Cilfacade.TypeOfError _  ->
-           VD.cast t v)
+           VD.cast ~kind t v)
       | SizeOf _
       | Real _
       | Imag _
@@ -999,7 +999,7 @@ struct
           else
             VD.top () (* upcasts not! *)
         in
-        let v' = VD.cast t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *)
+        let v' = VD.cast ~kind:Internal t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *) (* TODO: proper castkind *)
         if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!" VD.pretty v d_type t VD.pretty v';
         let v' = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (fun x -> get ~man st x (Some exp)) v' (convert_offset ~man st ofs) (Some exp) None t in (* handle offset *)
         v'
@@ -2061,7 +2061,7 @@ struct
             if not (ThreadIdDomain.Thread.is_main tid) then ( (* Only non-main return constitutes an implicit pthread_exit according to man page (https://github.com/goblint/analyzer/issues/1767#issuecomment-3642590227). *)
               (* Evaluate exp and cast the resulting value to the void-pointer-type.
                  Casting to the right type here avoids precision loss on joins. *)
-              let rv = VD.cast ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in
+              let rv = VD.cast ~kind:Internal ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in (* TODO: proper castkind *)
               man.sideg (V.thread tid) (G.create_thread rv)
             );
             Priv.thread_return ask (priv_getg man.global) (priv_sideg man.sideg) tid st'
@@ -2324,7 +2324,7 @@ struct
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
                   begin match man.ask (Queries.EvalLength ptr) with
                     | `Lifted arr_len ->
-                      let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in
+                      let arr_len_casted = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) arr_len in (* TODO: proper castkind *)
                       begin
                         try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
                         with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
@@ -2375,8 +2375,8 @@ struct
       let dest_size_equal_n =
         match dest_size, n_intdom with
         | `Lifted ds, `Lifted n ->
-          let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
-          let casted_n = ID.cast_to (Cilfacade.ptrdiff_ikind ()) n in
+          let casted_ds = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ds in (* TODO: proper castkind *)
+          let casted_n = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) n in (* TODO: proper castkind *)
           let ds_eq_n =
             begin try ID.eq casted_ds casted_n
               with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
@@ -2469,7 +2469,7 @@ struct
           let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
           let size = man.ask (Q.BlobSize {exp = s1; base_address = false}) in
           let s_id =
-            try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size
+            try ValueDomainQueries.ID.unlift (ID.cast_to ~kind:Internal ptrdiff_ik) size (* TODO: proper castkind *)
             with Failure _ -> ID.top_of ptrdiff_ik in
           let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
           set ~man st lv_a lv_typ (op_array empty_array array_s2)
@@ -2478,7 +2478,7 @@ struct
           let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
           let size = man.ask (Q.BlobSize {exp = s1; base_address = false}) in
           let s_id =
-            try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size
+            try ValueDomainQueries.ID.unlift (ID.cast_to ~kind:Internal ptrdiff_ik) size (* TODO: proper castkind *)
             with Failure _ -> ID.top_of ptrdiff_ik in
           let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
           let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
@@ -2642,7 +2642,7 @@ struct
         let eval_x = eval_rv ~man st x in
         begin match eval_x with
           | Int int_x ->
-            let xcast = ID.cast_to ik int_x in
+            let xcast = ID.cast_to ~kind:Internal ik int_x in (* TODO: proper castkind *)
             (* the absolute value of the most-negative value is out of range for 2'complement types *)
             (match (ID.minimal xcast), (ID.minimal (ID.top_of ik)) with
              | _, None
@@ -2661,11 +2661,11 @@ struct
           | Nan (fk, str) when Cil.isPointerType (Cilfacade.typeOf str) -> Float (FD.nan_of fk)
           | Nan _ -> failwith ("non-pointer argument in call to function "^f.vname)
           | Inf fk -> Float (FD.inf_of fk)
-          | Isfinite x -> Int (ID.cast_to IInt (apply_unary FDouble FD.isfinite x))
-          | Isinf x -> Int (ID.cast_to IInt (apply_unary FDouble FD.isinf x))
-          | Isnan x -> Int (ID.cast_to IInt (apply_unary FDouble FD.isnan x))
-          | Isnormal x -> Int (ID.cast_to IInt (apply_unary FDouble FD.isnormal x))
-          | Signbit x -> Int (ID.cast_to IInt (apply_unary FDouble FD.signbit x))
+          | Isfinite x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.isfinite x)) (* TODO: proper castkind *)
+          | Isinf x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.isinf x)) (* TODO: proper castkind *)
+          | Isnan x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.isnan x)) (* TODO: proper castkind *)
+          | Isnormal x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.isnormal x)) (* TODO: proper castkind *)
+          | Signbit x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.signbit x)) (* TODO: proper castkind *)
           | Ceil (fk,x) -> Float (apply_unary fk FD.ceil x)
           | Floor (fk,x) -> Float (apply_unary fk FD.floor x)
           | Fabs (fk, x) -> Float (apply_unary fk FD.fabs x)
@@ -2676,16 +2676,16 @@ struct
           | Cos (fk, x) -> Float (apply_unary fk FD.cos x)
           | Sin (fk, x) -> Float (apply_unary fk FD.sin x)
           | Tan (fk, x) -> Float (apply_unary fk FD.tan x)
-          | Isgreater (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.gt x y))
-          | Isgreaterequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.ge x y))
-          | Isless (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.lt x y))
-          | Islessequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.le x y))
-          | Islessgreater (x,y) -> Int(ID.c_logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y)))
-          | Isunordered (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.unordered x y))
+          | Isgreater (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.gt x y)) (* TODO: proper castkind *)
+          | Isgreaterequal (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.ge x y)) (* TODO: proper castkind *)
+          | Isless (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.lt x y)) (* TODO: proper castkind *)
+          | Islessequal (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.le x y)) (* TODO: proper castkind *)
+          | Islessgreater (x,y) -> Int(ID.c_logor (ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.gt x y))) (* TODO: proper castkind *)
+          | Isunordered (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.unordered x y)) (* TODO: proper castkind *)
           | Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
           | Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
           | Sqrt (fk, x) -> Float (apply_unary fk FD.sqrt x)
-          | Abs (ik, x) -> Int (ID.cast_to ik (apply_abs ik x))
+          | Abs (ik, x) -> Int (ID.cast_to ~kind:Internal ik (apply_abs ik x)) (* TODO: proper castkind *)
         end
       in
       Option.map_default (fun lv -> set ~man st (eval_lv ~man st lv) (Cilfacade.typeOfLval lv) result) st lv
@@ -2748,7 +2748,7 @@ struct
             let blob_set = Option.map_default (fun heap_var -> [heap_var, TVoid [], VD.Blob (VD.bot (), sizeval, ZeroInit.calloc)]) [] heap_var in
             set_many ~man st ((eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address addr):: blob_set)
           else
-            let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
+            let blobsize = ID.mul (ID.cast_to ~kind:Internal ik @@ sizeval) (ID.cast_to ~kind:Internal ik @@ countval) in (* TODO: proper castkind *)
             let offset = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
             (* the heap_var is the base address of the allocated memory, but we need to keep track of the offset for the blob *)
             let addr_offset = AD.map (fun a -> Addr.add_offset a offset) addr in

src/analyses/baseInvariant.ml

@@ -125,7 +125,7 @@ struct
                 let st = set' lv lval_a st in
                 let orig = AD.Addr.add_offset base_a original_offset in
                 let old_val = get ~man st (AD.singleton orig) None in
-                let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *)
+                let old_val = VD.cast ~kind:Internal (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *) (* TODO: proper castkind *)
                 (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *)
                 (* let old_val = eval_rv_lval_refine ~man st exp x in *)
                 let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
@@ -157,7 +157,7 @@ struct
         (match value with
          | Int n ->
            let ikind = Cilfacade.get_ikind_exp (Lval lval) in
-           `Refine (x, Int (ID.cast_to ikind n))
+           `Refine (x, Int (ID.cast_to ~kind:Internal ikind n)) (* TODO: proper castkind *)
          | _ -> `Refine (x, value))
       (* The false-branch for x == value: *)
       | Eq, x, value, false -> begin
@@ -194,7 +194,7 @@ struct
           match value with
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
-              let n = ID.cast_to ikind n in
+              let n = ID.cast_to ~kind:Internal ikind n in (* TODO: proper castkind *)
               let range_from x = if tv then ID.ending ikind (Z.pred x) else ID.starting ikind x in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
@@ -209,7 +209,7 @@ struct
           match value with
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
-              let n = ID.cast_to ikind n in
+              let n = ID.cast_to ~kind:Internal ikind n in (* TODO: proper castkind *)
               let range_from x = if tv then ID.ending ikind x else ID.starting ikind (Z.succ x) in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
@@ -241,7 +241,7 @@ struct
         let v = eval_rv ~man st rval in
         let x_type = Cilfacade.typeOfLval x in
         if VD.is_dynamically_safe_cast x_type (Cilfacade.typeOf rval) v then
-          helper op x (VD.cast x_type v) tv
+          helper op x (VD.cast ~kind:Internal x_type v) tv (* TODO: proper castkind *)
         else
           `NotUnderstood
       | BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv
@@ -759,7 +759,7 @@ struct
              | a1, a2 -> fallback (fun () -> Pretty.dprintf "binop: got abstract values that are not Int: %a and %a" VD.pretty a1 VD.pretty a2) st)
             (* use closures to avoid unused casts *)
           in (match c_typed with
-              | Int c -> invert_binary_op c ID.pretty (fun ik -> ID.cast_to ik c) (fun fk -> FD.of_int fk c)
+              | Int c -> invert_binary_op c ID.pretty (fun ik -> ID.cast_to ~kind:Internal ik c) (fun fk -> FD.of_int fk c) (* TODO: proper castkind *)
               | Float c -> invert_binary_op c FD.pretty (fun ik -> FD.to_int ik c) (fun fk -> FD.cast_to fk c)
               | _ -> failwith "unreachable")
         | Lval x, (Int _ | Float _ | Address _) -> (* meet x with c *)
@@ -771,7 +771,7 @@ struct
               let c' = match t with
                 | TPtr _ -> VD.Address (AD.of_int c)
                 | TInt (ik, _)
-                | TEnum ({ekind = ik; _}, _) -> Int (ID.cast_to ik c)
+                | TEnum ({ekind = ik; _}, _) -> Int (ID.cast_to ~kind:Internal ik c) (* TODO: proper castkind *)
                 | TFloat (fk, _) -> Float (FD.of_int fk c)
                 | _ -> Int c
               in
@@ -783,7 +783,7 @@ struct
                   if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pretty tmpSpecial;
                   begin match tmpSpecial with
                     | `Lifted (Abs (ik, xInt)) ->
-                      let c' = ID.cast_to ik c in (* different ik! *)
+                      let c' = ID.cast_to ~kind:Internal ik c in (* different ik! *) (* TODO: proper castkind *)
                       inv_exp (Int (ID.join c' (ID.neg c'))) xInt st
                     | tmpSpecial ->
                       BatOption.map_default_delayed (fun tv ->
@@ -856,8 +856,8 @@ struct
                     if VD.is_dynamically_safe_cast t t' (Int i) then
                       (* let c' = ID.cast_to ik_e c in *)
                       (* Suppressing overflow warnings as this is not a computation that comes from the program *)
-                      let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in
-                      let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *)
+                      let res_range = (ID.cast_to ~suppress_ovwarn:true ~kind:Internal ik (ID.top_of ik_e)) in (* TODO: proper castkind *)
+                      let c' = ID.cast_to ~kind:Internal ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *) (* TODO: proper castkind *)
                       if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
                       inv_exp (Int c') e st
                     else