Minimize unnecessary casts and check for overflows in witness invariants

src/analyses/apron/relationAnalysis.apron.ml

@@ -173,25 +173,8 @@ struct
     | _ ->
       st
 
-
-  (** An extended overflow handling inside relationAnalysis for expression assignments when overflows are assumed to occur.
-      Since affine equalities can only keep track of integer bounds of expressions evaluating to definite constants, we now query the integer bounds information for expressions from other analysis.
-      If an analysis returns bounds that are unequal to min and max of ikind , we can exclude the possibility that an overflow occurs and the abstract effect of the expression assignment can be used, i.e. we do not have to set the variable's value to top. *)
-
-  let no_overflow (ask: Queries.ask) exp =
-    match Cilfacade.get_ikind_exp exp with
-    | exception Invalid_argument _ -> false (* is thrown by get_ikind_exp when the type of the expression is not an integer type *)
-    | exception Cilfacade.TypeOfError _ -> false
-    | ik ->
-      if IntDomain.should_wrap ik then
-        false
-      else if IntDomain.should_ignore_overflow ik then
-        true
-      else
-        not (ask.f (MaySignedOverflow exp))
-
   let no_overflow man exp = lazy (
-    let res = no_overflow man exp in
+    let res = SharedFunctions.no_overflow man exp in
     if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a" res d_exp exp;
     res
   )
@@ -631,7 +614,7 @@ struct
         (* filter one-vars and exact *)
         (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
         if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
-          RD.cil_exp_of_lincons1 lincons1
+          RD.cil_exp_of_lincons1 ask e_inv lincons1
           |> Option.map e_inv
           |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)
         else

src/analyses/apron/relationPriv.apron.ml

@@ -730,7 +730,7 @@ struct
               (* filter one-vars and exact *)
               (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
               if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
-                RD.cil_exp_of_lincons1 lincons1
+                RD.cil_exp_of_lincons1 ask Fun.id lincons1
                 |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp))
               else
                 None

src/analyses/base.ml

@@ -1298,7 +1298,7 @@ struct
       For now we return true if the expression contains a shift left.
   *)
   (* TODO: deduplicate https://github.com/goblint/analyzer/pull/1297#discussion_r1477804502 *)
-  let rec exp_may_signed_overflow man exp =
+  let rec exp_may_overflow man exp ~unsigned =
     let res = match Cilfacade.get_ikind_exp exp with
       | exception (Cilfacade.TypeOfError _) (* Cilfacade.typeOf *)
       | exception (Invalid_argument _) -> (* get_ikind *)
@@ -1360,20 +1360,20 @@ struct
         | Imag e
         | SizeOfE e
         | AlignOfE e
-        | CastE (_, e) -> exp_may_signed_overflow man e
+        | CastE (_, e) -> exp_may_overflow man e ~unsigned:unsigned
         | UnOp (unop, e, _) ->
           (* check if the current operation causes a signed overflow *)
           begin match unop with
             | Neg -> (* an overflow happens when the lower bound of the interval is less than MIN_INT *)
-              Cil.isSigned ik && checkPredicate e (Z.gt)
+              (unsigned || Cil.isSigned ik) && checkPredicate e (Z.gt)
             (* operations that do not result in overflow in C: *)
             | BNot|LNot -> false
           end
           (* look for overflow in subexpression *)
-          || exp_may_signed_overflow man e
+          || exp_may_overflow man e ~unsigned:unsigned
         | BinOp (binop, e1, e2, _) ->
           (* check if the current operation causes a signed overflow *)
-          (Cil.isSigned ik && begin match binop with
+          ((unsigned || Cil.isSigned ik) && begin match binop with
               | PlusA|PlusPI|IndexPI -> checkBinop e1 e2 (GobOption.map2 Z.(+))
               | MinusA|MinusPI|MinusPP -> checkBinop e1 e2 (GobOption.map2 Z.(-))
               | Mult -> checkBinop e1 e2 (GobOption.map2 Z.mul)
@@ -1385,27 +1385,27 @@ struct
               (* Shiftlt can cause overflow and also undefined behaviour in case the second operand is non-positive*)
               | Shiftlt -> true end)
           (* look for overflow in subexpression *)
-          || exp_may_signed_overflow man e1 || exp_may_signed_overflow man e2
+          || exp_may_overflow man e1 ~unsigned:unsigned || exp_may_overflow man e2 ~unsigned:unsigned
         | Question (e1, e2, e3, _) ->
           (* does not result in overflow in C *)
-          exp_may_signed_overflow man e1 || exp_may_signed_overflow man e2 || exp_may_signed_overflow man e3
+          exp_may_overflow man e1 ~unsigned:unsigned || exp_may_overflow man e2 ~unsigned:unsigned || exp_may_overflow man e3 ~unsigned:unsigned
         | Lval lval
         | AddrOf lval
-        | StartOf lval -> lval_may_signed_overflow man lval
+        | StartOf lval -> lval_may_overflow man lval ~unsigned:unsigned
     in
-    if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp exp res; res
-  and lval_may_signed_overflow man (lval : lval) =
+    if M.tracing then M.trace "signed_overflow" "base exp_may_overflow %a. Result = %b" d_plainexp exp res; res
+  and lval_may_overflow man (lval : lval) ~unsigned =
     let (host, offset) = lval in
-    let host_may_signed_overflow = function
+    let host_may_overflow = function
       | Var v -> false
-      | Mem e -> exp_may_signed_overflow man e
+      | Mem e -> exp_may_overflow man e ~unsigned:unsigned
     in
-    let rec offset_may_signed_overflow = function
+    let rec offset_may_overflow = function
       | NoOffset -> false
-      | Index (e, o) -> exp_may_signed_overflow man e || offset_may_signed_overflow o
-      | Field (f, o) -> offset_may_signed_overflow o
+      | Index (e, o) -> exp_may_overflow man e ~unsigned:unsigned || offset_may_overflow o
+      | Field (f, o) -> offset_may_overflow o
     in
-    host_may_signed_overflow host || offset_may_signed_overflow offset
+    host_may_overflow host || offset_may_overflow offset
 
   let query man (type a) (q: a Q.t): a Q.result =
     match q with
@@ -1577,9 +1577,12 @@ struct
     | Q.InvariantGlobal g ->
       let g: V.t = Obj.obj g in
       query_invariant_global man g
-    | Q.MaySignedOverflow e -> (let res = exp_may_signed_overflow man e in
-                                if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp e res; res
-                               )
+    | Q.MaySignedOverflow e ->
+      let res = exp_may_overflow man e ~unsigned:false in
+      if M.tracing then M.trace "signed_overflow" "base exp_may_overflow %a. Result = %b" d_plainexp e res; res
+    | Q.MayOverflow e ->
+      let res = exp_may_overflow man e ~unsigned:true in
+      if M.tracing then M.trace "overflow" "base exp_may_overflow %a. Result = %b" d_plainexp e res; res
     | _ -> Q.Result.top q
 
   let update_variable variable typ value cpa =

src/cdomains/apron/apronDomain.apron.ml

@@ -216,7 +216,7 @@ sig
   val to_lincons_array : t -> Lincons1.earray
   val of_lincons_array : Lincons1.earray -> t
 
-  val cil_exp_of_lincons1: Lincons1.t -> exp option
+  val cil_exp_of_lincons1: Queries.ask -> (exp -> exp) -> Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end
 

src/cdomains/apron/relationDomain.apron.ml

@@ -139,7 +139,7 @@ end
 module type S3 =
 sig
   include S2
-  val cil_exp_of_lincons1: Lincons1.t -> exp option
+  val cil_exp_of_lincons1: Queries.ask -> (exp -> exp) -> Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end
 

src/cdomains/apron/sharedFunctions.apron.ml

@@ -42,6 +42,20 @@ let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) =
     | _ ->
       failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar)
 
+(** An extended overflow handling inside relationAnalysis for expression assignments when overflows are assumed to occur.
+    Since affine equalities can only keep track of integer bounds of expressions evaluating to definite constants, we now query the integer bounds information for expressions from other analysis.
+    If an analysis returns bounds that are unequal to min and max of ikind , we can exclude the possibility that an overflow occurs and the abstract effect of the expression assignment can be used, i.e. we do not have to set the variable's value to top. *)
+let no_overflow (ask: Queries.ask) exp =
+  match Cilfacade.get_ikind_exp exp with
+  | exception Invalid_argument _ -> false (* is thrown by get_ikind_exp when the type of the expression is not an integer type *)
+  | exception Cilfacade.TypeOfError _ -> false
+  | ik ->
+    if IntDomain.should_wrap ik then
+      false
+    else if IntDomain.should_ignore_overflow ik then
+      true
+    else
+      not (ask.f (MaySignedOverflow exp))
 
 module type ConvertArg =
 sig
@@ -253,47 +267,96 @@ struct
 
   let longlong = TInt(ILongLong,[])
 
+  let check_for_overflows_no_further_cast (ask: Queries.ask) (e_inv: exp -> exp) cast_exp exp_plain =
+    if not (ask.f (MayOverflow (e_inv cast_exp))) then
+      cast_exp, exp_plain
+    else (
+      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" CilType.Exp.pretty cast_exp;
+      raise Unsupported_Linexpr1
+    )
+
+  let is_cast_injective_vtype vinfo = IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:longlong
+
+  let rec check_for_overflows (ask: Queries.ask) (e_inv: exp -> exp) exp exp_plain =
+    if not (ask.f (MayOverflow (e_inv exp))) then
+      exp, exp_plain
+    else
+      match exp, exp_plain with
+      | Lval (Var vinfo, NoOffset) as var, _ when is_cast_injective_vtype vinfo ->
+        let cast_var = Cilfacade.mkCast ~e:var ~newt:longlong in
+        check_for_overflows_no_further_cast ask e_inv cast_var cast_var
+      | BinOp (op, (Const i as c), ((Lval (Var vinfo, NoOffset)) as var), _), _ when is_cast_injective_vtype vinfo ->
+        let cast_var = Cilfacade.mkCast ~e:var ~newt:longlong in
+        let cast_exp_plain = BinOp (op, c, cast_var, longlong) in
+        let cast_exp = Cilfacade.makeBinOp op c cast_var in
+        check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
+      | BinOp (op, ((Lval (Var vinfo1, NoOffset)) as var1), ((Lval (Var vinfo2, NoOffset)) as var2), _), BinOp (_, _, var2_plain, _) when is_cast_injective_vtype vinfo1 && is_cast_injective_vtype vinfo2 ->
+        let cast_var = Cilfacade.mkCast ~e:var1 ~newt:longlong in
+        let cast_exp_plain = BinOp (op, cast_var, var2_plain, longlong) in
+        let cast_exp = Cilfacade.makeBinOp op cast_var var2 in
+        check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
+      | BinOp (op, exp1, exp2, _), BinOp (_, _, exp2_plain, _) ->
+        let cast_exp1 = Cilfacade.mkCast ~e:exp1 ~newt:longlong in
+        let cast_exp_plain = BinOp (op, cast_exp1, exp2_plain, longlong) in
+        let cast_exp = Cilfacade.makeBinOp op cast_exp1 exp2 in
+        check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
+      | _ ->
+        M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil expression in overflow preserving manner: %a" CilType.Exp.pretty exp;
+        raise Unsupported_Linexpr1
+
+  (* Determines the integer kind (ikind) for a given constant.
+     - Defaults to IInt for values that fit int range to minimize the number of LL suffixes in invariants.
+     - Uses ILongLong to handle larger constants and prevent integer overflows.
+     - If the constant cannot fit into ILongLong, it is discarded with a warning. *)
+  let const_ikind i =
+    match () with
+    | _ when Cil.fitsInInt IInt i -> IInt
+    | _ when Cil.fitsInInt ILongLong i -> ILongLong
+    | _ ->
+      M.warn ~category:Analyzer "Invariant Apron: coefficient does not fit long long type: %s" (Z.to_string i);
+      raise Unsupported_Linexpr1
 
   let coeff_to_const ~scalewith (c:Coeff.union_5) =
     match c with
     | Scalar c ->
       (match int_of_scalar ?scalewith c with
       | Some i ->
-        let ci,truncation = truncateCilint ILongLong i in
+        let ikind = const_ikind i in
+        let ci,truncation = truncateCilint ikind i in
         if truncation = NoTruncation then
           if Z.compare i Z.zero >= 0 then
-            false, Const (CInt(i,ILongLong,None))
+            false, Const (CInt(i,ikind,None))
           else
             (* attempt to negate if that does not cause an overflow *)
-            let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
+            let cneg, truncation = truncateCilint ikind (Z.neg i) in
             if truncation = NoTruncation then
-              true, Const (CInt((Z.neg i),ILongLong,None))
+              true, Const (CInt((Z.neg i),ikind,None))
             else
-              false, Const (CInt(i,ILongLong,None))
+              false, Const (CInt(i,ikind,None))
         else
           (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
       | None -> raise Unsupported_Linexpr1)
     | _ -> raise Unsupported_Linexpr1
 
-  let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =
+  let cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) (e_inv: exp -> exp) (c: Coeff.t) v =
     match V.to_cil_varinfo v with
-    | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
-      let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
+    | Some vinfo ->
+      let var = Lval (Var vinfo, NoOffset) in
       let flip, coeff = coeff_to_const ~scalewith c in
-      let prod = BinOp(Mult, coeff, var, longlong) in
-      flip, prod
+      let exp = Cilfacade.makeBinOp Mult coeff var in
+      let exp_plain = BinOp (Mult, coeff, var, Cilfacade.typeOf exp) in
+      let prod, prod_plain = check_for_overflows ask e_inv exp exp_plain in
+      flip, (prod, prod_plain)
     | None ->
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
       raise Unsupported_Linexpr1
-    | _ ->
-      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v;
-      raise Unsupported_Linexpr1
 
-  let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
-    let terms = ref [coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1)] in
+  let cil_exp_of_linexpr1 ?scalewith (ask: Queries.ask) (e_inv: exp -> exp) (linexpr1:Linexpr1.t) =
+    let flip, coeff = coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1) in
+    let terms = ref [flip, (coeff, coeff)] in
     let append_summand (c:Coeff.union_5) v =
       if not (Coeff.is_zero c) then
-        terms := cil_exp_of_linexpr1_term ~scalewith c v :: !terms
+        terms := cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) e_inv c v :: !terms
     in
     Linexpr1.iter append_summand linexpr1;
     !terms
@@ -325,19 +388,23 @@ struct
       Linexpr1.iter lcm_coeff linexpr1; !lcm_denom
     with UnsupportedScalar -> Z.one
 
-  let cil_exp_of_lincons1 (lincons1:Lincons1.t) =
-    let zero = Cil.kinteger ILongLong 0 in
+  let cil_exp_of_lincons1 (ask: Queries.ask) (e_inv: exp -> exp) (lincons1:Lincons1.t)  =
+    let zero = Cil.kinteger IInt 0 in
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let common_denominator = lcm_den linexpr1 in
-      let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
+      let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator (ask: Queries.ask) e_inv linexpr1 in
       let (nterms, pterms) = Tuple2.mapn (List.map snd) (List.partition fst terms) in
       let fold_terms terms =
-        List.fold_left (fun acc term ->
+        List.fold_left (fun acc (term, term_plain) ->
             match acc with
-            | None -> Some term
-            | Some exp -> Some (BinOp (PlusA, exp, term, longlong))
+            | None -> Some (check_for_overflows ask e_inv term term_plain)
+            | Some (exp, exp_plain) ->
+              let exp' = Cilfacade.makeBinOp PlusA exp term in
+              let exp_plain' = BinOp (PlusA, exp_plain, term_plain, Cilfacade.typeOf exp') in
+              Some (check_for_overflows ask e_inv exp' exp_plain')
           ) None terms
+        |> Option.map Tuple2.second
         |> Option.default zero
       in
       let lhs = fold_terms pterms in

src/domains/queries.ml

@@ -130,6 +130,7 @@ type _ t =
   | IsEverMultiThreaded: MayBool.t t
   | TmpSpecial: Mval.Exp.t -> ML.t t
   | MaySignedOverflow: exp -> MayBool.t t
+  | MayOverflow: exp -> MayBool.t t
   | GasExhausted: CilType.Fundec.t ->  MustBool.t t
   | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *)
   | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t
@@ -205,6 +206,7 @@ struct
     | IsEverMultiThreaded -> (module MayBool)
     | TmpSpecial _ -> (module ML)
     | MaySignedOverflow  _ -> (module MayBool)
+    | MayOverflow  _ -> (module MayBool)
     | GasExhausted _ -> (module MustBool)
     | YamlEntryGlobal _ -> (module YS)
     | GhostVarAvailable _ -> (module MayBool)
@@ -279,6 +281,7 @@ struct
     | IsEverMultiThreaded -> MayBool.top ()
     | TmpSpecial _ -> ML.top ()
     | MaySignedOverflow _ -> MayBool.top ()
+    | MayOverflow _ -> MayBool.top ()
     | GasExhausted _ -> MustBool.top ()
     | YamlEntryGlobal _ -> YS.top ()
     | GhostVarAvailable _ -> MayBool.top ()
@@ -349,11 +352,12 @@ struct
     | Any (TmpSpecial _) -> 56
     | Any (IsAllocVar _) -> 57
     | Any (MaySignedOverflow _) -> 58
-    | Any (GasExhausted _) -> 59
-    | Any (YamlEntryGlobal _) -> 60
-    | Any (MustProtectingLocks _) -> 61
-    | Any (GhostVarAvailable _) -> 62
-    | Any InvariantGlobalNodes -> 63
+    | Any (MayOverflow _) -> 59
+    | Any (GasExhausted _) -> 60
+    | Any (YamlEntryGlobal _) -> 61
+    | Any (MustProtectingLocks _) -> 62
+    | Any (GhostVarAvailable _) -> 63
+    | Any InvariantGlobalNodes -> 64
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -410,6 +414,7 @@ struct
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
       | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
       | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2
+      | Any (MayOverflow e1), Any (MayOverflow e2) -> CilType.Exp.compare e1 e2
       | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2
       | Any (GhostVarAvailable v1), Any (GhostVarAvailable v2) -> WitnessGhostVar.compare v1 v2
       (* only argumentless queries should remain *)
@@ -456,6 +461,7 @@ struct
     | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
     | Any (TmpSpecial lv) -> Mval.Exp.hash lv
     | Any (MaySignedOverflow e) -> CilType.Exp.hash e
+    | Any (MayOverflow e) -> CilType.Exp.hash e
     | Any (GasExhausted f) -> CilType.Fundec.hash f
     | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v
     (* IterSysVars:                                                                    *)
@@ -523,6 +529,7 @@ struct
     | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
     | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
     | Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e
+    | Any (MayOverflow e) -> Pretty.dprintf "MayOverflow %a" CilType.Exp.pretty e
     | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f
     | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v
     | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes"