Implemented oerflow handling and added corresponding tests

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -88,7 +88,7 @@ struct
 end
 
 (** As it is specifically used for the new affine equality domain, it can only provide bounds if the expression contains known constants only and in that case, min and max are the same. *)
-module ExpressionBounds (Vc: AbstractVector) (Mx: AbstractMatrix): (SharedFunctions.ConvBounds with type t = VarManagement(Vc) (Mx).t) =
+module ExpressionBounds (Vc: AbstractVector) (Mx: AbstractMatrix): (SharedFunctions.ExtendedConvBounds with type t = VarManagement(Vc) (Mx).t) =
 struct
   include VarManagement (Vc) (Mx)
 
@@ -437,24 +437,7 @@ struct
       Additionally, we now also refine after positive guards when overflows might occur and there is only one variable inside the expression and the expression is an equality constraint check (==).
       We check after the refinement if the new value of the variable is outside its integer bounds and if that is the case, either revert to the old state or set it to bottom. *)
 
-  exception NotRefinable
-
-  let meet_tcons_one_var_eq res expr =
-    let overflow_res res = if IntDomain.should_ignore_overflow (Cilfacade.get_ikind_exp expr) then res else raise NotRefinable in
-    match Convert.find_one_var expr with
-    | None -> overflow_res res
-    | Some v ->
-      let ik = Cilfacade.get_ikind v.vtype in
-      match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res res.env (Lval (Cil.var v)) true) with
-      | Some _, Some _ when not (Cil.isSigned ik) -> raise NotRefinable (* TODO: unsigned w/o bounds handled differently? *)
-      | Some min, Some max ->
-        assert (Z.equal min max); (* other bounds impossible in affeq *)
-        let (min_ik, max_ik) = IntDomain.Size.range ik in
-        if Z.compare min min_ik < 0 || Z.compare max max_ik > 0 then
-          if IntDomain.should_ignore_overflow ik then bot () else raise NotRefinable
-        else res
-      | exception Convert.Unsupported_CilExp _
-      | _, _ -> overflow_res res
+  module BoundsCheck = SharedFunctions.BoundsCheckMeetTcons (Bounds) (V)
 
   let meet_tcons t tcons expr =
     let check_const cmp c = if cmp c Mpqf.zero then bot_env else t
@@ -465,7 +448,7 @@ struct
       let res = if is_bot t then bot () else
           let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e
           in if Option.is_none opt_m then bot () else {d = opt_m; env = t.env} in
-      meet_tcons_one_var_eq res expr
+      BoundsCheck.meet_tcons_one_var_eq res expr
     in
     match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with
     | Some v ->
@@ -477,12 +460,12 @@ struct
         | None, DISEQ
         | None, SUP ->
           begin match meet_vec v with
-            | exception NotRefinable -> t
+            | exception BoundsCheck.NotRefinable -> t
             | res -> if equal res t then bot_env else t
           end
         | None, EQ ->
           begin match meet_vec v with
-            | exception NotRefinable -> t
+            | exception BoundsCheck.NotRefinable -> t
             | res -> if is_bot res then bot_env else res
           end
         | _, _ -> t

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

@@ -25,7 +25,7 @@ module Equality = struct
   let zero = (None, Z.zero)
   let var_zero i = (Some i, Z.zero)
   let to_int x = Z.to_int @@ snd x
-  let print : t -> unit = fun (a, b) -> match a with
+  let print (a, b) = match a with
     | None -> print_endline @@ "(None , " ^ Z.to_string b ^ ")"
     | Some x -> print_endline @@ "(Some " ^ string_of_int x ^ ", " ^ Z.to_string b ^ ")"
 end
@@ -39,7 +39,7 @@ module EqualitiesArray = struct
   let empty () = [||]
 
   let make_empty_array len = let array = (make len Equality.zero) in
-      BatArray.modifyi (fun i (x, y) -> (Some i, Z.zero)) array; array
+    BatArray.modifyi (fun i (x, y) -> (Some i, Z.zero)) array; array
 
   let add_empty_column arr index = 
     let num_vars = length arr in
@@ -266,11 +266,14 @@ end
 
 
 (** TODO: overflow checking *)
-module ExpressionBounds: (SharedFunctions.ConvBounds with type t = VarManagement.t) =
+module ExpressionBounds: (SharedFunctions.ExtendedConvBounds with type t = VarManagement.t) =
 struct
   include VarManagement
 
-  let bound_texpr t texpr = None, None(*Some (Z.of_int (-1000)), Some (Z.of_int (1000)) TODO*)
+  let bound_texpr t texpr = let texpr = Texpr1.to_expr texpr in
+    match get_coeff t texpr with
+    | Some (None, offset) -> Some offset, Some offset
+    | _ -> None, None
 
 
   let bound_texpr d texpr1 =
@@ -330,11 +333,11 @@ struct
     let t1, t2 = change_d t1 sup_env ~add:true ~del:false, change_d t2 sup_env ~add:true ~del:false in
     let subst_var ts x t = 
       let adjust e = match e with
-      | (None, b') -> (None, b')
-      | (Some x', b') -> if x = x' then
-          (match t with 
-           | (None, bt) -> (None, Z.(b' + bt))
-           | (Some xt, bt) -> (Some xt, Z.(b' + bt))) 
+        | (None, b') -> (None, b')
+        | (Some x', b') -> if x = x' then
+            (match t with 
+             | (None, bt) -> (None, Z.(b' + bt))
+             | (Some xt, bt) -> (Some xt, Z.(b' + bt))) 
           else (Some x', b')in
       Stdlib.Option.iter (BatArray.modify adjust) !ts (*
       match !ts with
@@ -355,7 +358,7 @@ struct
         (match t with
          | (None, b) -> 
            (match ts'.(i) with
-            | (None, b') -> if Z.(b <> b') then ts := None;
+            | (None, b') -> if not @@ Z.equal b b' then ts := None;
             | (Some j, b') -> subst_var ts j (None, Z.(b - b')))
          | (Some j, b) ->
            (match ts'.(i) with
@@ -368,14 +371,14 @@ struct
                    (if Z.(b1 <> (b2 + b)) then ts := None)
                  else if h1 < h2 then subst_var ts h2 (Some h1, Z.(b1 - (b + b2)))
                  else subst_var ts h1 (Some h2, Z.(b + (b2 - b1))))))
-                in
-       Stdlib.Option.iter adjust !ts
+      in
+      Stdlib.Option.iter adjust !ts
     in 
     match t1.d, t2.d with
     | Some d1', Some d2' -> (
-      let ds = ref (Some (Array.copy d1')) in
-      Array.iteri (fun j e -> add_conj ds e j) d2'; 
-      {d = !ds; env = sup_env} )
+        let ds = ref (Some (Array.copy d1')) in
+        Array.iteri (fun j e -> add_conj ds e j) d2'; 
+        {d = !ds; env = sup_env} )
     | _ -> { d = None; env = sup_env} 
 
   let meet t1 t2 =
@@ -391,7 +394,7 @@ struct
       match t with
       | (None, b) -> 
         (match ts.(i) with
-         | (None, b') -> Z.(b = b')
+         | (None, b') -> Z.equal b b'
          | _ -> false)
       | (Some j, b) -> 
         (match ts.(i), ts.(j) with
@@ -434,11 +437,11 @@ struct
         | (Some ii, _), (Some ij, _) -> ii - ij 
       in
       let diff_e1 = cmp_z_ref t1i t1j in
-        if diff_e1 <> 0 then diff_e1 
-        else
-          let diff_e2 = cmp_z_ref t2i t2j in
-          if diff_e2 <> 0 then diff_e2 else 
-            Z.to_int (Z.((diff t1i t2i) - (diff t1j t2j)))
+      if diff_e1 <> 0 then diff_e1 
+      else
+        let diff_e2 = cmp_z_ref t2i t2j in
+        if diff_e2 <> 0 then diff_e2 else 
+          Z.to_int (Z.((diff t1i t2i) - (diff t1j t2j)))
     in
     let sort_z_by_expr zts =
       Stdlib.Option.iter (Array.stable_sort cmp_z) zts 
@@ -456,28 +459,28 @@ struct
       in
       let size_of_eq_class zts (start : int) : int =
         let iterate result i e =
-           if i >= start && cmp_z zts.(start) e == 0 then result + 1
-           else result in
+          if i >= start && cmp_z zts.(start) e == 0 then result + 1
+          else result in
         Array.fold_lefti iterate 0 zts
       in
       let least_index_var_in_eq_class zts start size : int * Z.t =
         let (i, (_, b), (_, _)) = zts.(start)in
         let result = (i,b) in
         let iterate (a, b) i (j, (_, bj), (_, _))=
-         if i > start && j < a then (j,bj) else (a,b) in
+          if i > start && j < a then (j,bj) else (a,b) in
         Array.fold_lefti iterate result zts 
       in
       let all_are_const_in_eq_class zts start size : bool = 
         Array.fold_left (fun b e -> b && (is_const e)) true zts
       in
       let assign_vars_in_const_eq_class ats zts start size least_i least_b =  
         let adjust i e =  if i < start then e 
-        else 
-          let (ai, t1, t2) = zts.(i)in
-          if Z.equal (diff t1 t2) (Z.zero) then (ai, t1)
-          else
-             (ai, (Some least_i, Z.sub (Tuple2.second t1) least_b))
-        (*  
+          else 
+            let (ai, t1, t2) = zts.(i)in
+            if Z.equal (diff t1 t2) (Z.zero) then (ai, t1)
+            else
+              (ai, (Some least_i, Z.sub (Tuple2.second t1) least_b))
+              (*  
         for i = start to start + size - 1 do
           let (ai, t1, t2) = zts.(i) in
           if Z.equal (diff t1 t2) (Z.zero) then ats.(i) <- (ai, t1)
@@ -504,8 +507,8 @@ struct
           (if n = 1 then
              let (i', t1, t2) = zts'.(!i) in
              if is_const (i', t1, t2) && Z.equal (diff t1 t2) (Z.zero) then 
-                 result.(!i) <- (i', (None, const_offset t1))
-               else result.(!i) <- (i', (Some i', Z.zero))
+               result.(!i) <- (i', (None, const_offset t1))
+             else result.(!i) <- (i', (Some i', Z.zero))
            else
              let (least_i, least_b) = least_index_var_in_eq_class zts' !i n in
              (if all_are_const_in_eq_class zts' !i n then
@@ -709,10 +712,17 @@ struct
      tcons -> tree constraint (expression < 0)
      -> does not have types (overflow is type dependent)
   *)
-  let meet_tcons t tcons _ = 
+  module BoundsCheck = SharedFunctions.BoundsCheckMeetTcons (Bounds) (V)
+
+  let meet_tcons t tcons original_expr = 
     (* The expression is evaluated using an array of coefficients. The first element of the array belongs to the constant followed by the coefficients of all variables 
        depending on the result in the array after the evaluating including resolving the constraints in t.d the tcons can be evaluated and additional constraints can be added to t.d *)
-    let expr = Array.init ((Environment.size t.env) +1) (fun _ -> Z.zero) in 
+    let overflow_handling res original_expr =
+      match BoundsCheck.meet_tcons_one_var_eq res original_expr with
+      | exception BoundsCheck.NotRefinable -> t
+      | res -> res
+    in
+    let expr = Array.init ((Environment.size t.env) + 1) (fun _ -> Z.zero) in 
     match t.d with 
     | None -> bot_env
     | Some d -> if is_bot_env t then bot_env else
@@ -727,7 +737,7 @@ struct
               | (None, c_i) -> Array.set expr 0 (Z.add expr.(0)  (Z.mul c  c_i))
           in 
           List.iter (update expr) cv's ;
-          let counting count i a = if i = 0 || Z.equal a Z.zero then count else count+1 in
+          let counting count i a = if i = 0 || Z.equal a Z.zero then count else count + 1 in
           let var_count = Array.fold_lefti counting 0 expr
           in 
           if var_count = 0 then 
@@ -745,18 +755,21 @@ struct
             let c = if Z.divisible expr.(0) @@ Tuple2.second var then Some (Z.(- expr.(0) / (Tuple2.second var))) else None in
             match Tcons1.get_typ tcons, c with 
             | EQ, Some c-> 
-                let expr = Texpr1.to_expr @@ Texpr1.cst t.env  (Coeff.s_of_int @@ Z.to_int c) in 
-                meet t (assign_texpr (identity t.env) (Environment.var_of_dim t.env (Tuple2.first var)) expr) 
+              let expression = Texpr1.to_expr @@ Texpr1.cst t.env  (Coeff.s_of_int @@ Z.to_int c) in 
+              let res = meet t (assign_texpr (identity t.env) (Environment.var_of_dim t.env (Tuple2.first var)) expression) 
+              in overflow_handling res original_expr
             | _ -> t (*Not supported right now*)
           else if var_count = 2 then 
-            let get_vars i a l = if Z.equal a Z.zero || i = 0 then l else (i,a)::l in
-          let v12 =  Array.fold_righti get_vars expr [] in
+            let get_vars i a l = if Z.equal a Z.zero || i = 0 then l else (i - 1,a)::l in
+            let v12 = Array.fold_righti get_vars expr [] in
             let a1 = Tuple2.second (List.hd v12) in  
             let a2 = Tuple2.second (List.hd @@ List.tl v12) in
             let var1 = Environment.var_of_dim t.env (Tuple2.first (List.hd v12)) in 
             let var2 = Environment.var_of_dim t.env (Tuple2.first (List.hd @@ List.tl v12)) in
             match Tcons1.get_typ tcons with 
-            | EQ -> if Z.equal a1 Z.one && Z.equal a2  Z.one then meet t (assign_var (identity t.env) var1 var2) else t
+            | EQ -> 
+              let res = if Z.equal a1 Z.one && Z.equal a2  Z.one then meet t (assign_var (identity t.env) var1 var2) else t
+              in overflow_handling res original_expr
             | _-> t (*Not supported right now*)
           else 
             t (*For any other case we don't know if the (in-) equality is true or false or even possible therefore we just return t *)

src/cdomains/apron/sharedFunctions.apron.ml

@@ -291,6 +291,7 @@ struct
   let bot () =
     {d = Some (RelDomain.empty ()); env = empty_env}
 
+  let get_env t = t.env
   let bot_env = {d = None; env = empty_env}
 
   let is_bot_env t = t.d = None
@@ -488,3 +489,36 @@ module Mpqf = struct
   let get_num x = Z_mlgmpidl.z_of_mpzf @@ Mpqf.get_num x
   let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x)
 end
+
+
+(** Overflow handling for meet_tcons in affineEqualityDomain and linearTwoVarEqualityDomain.
+
+    It refines after positive guards when overflows might occur and there is only one variable inside the expression and the expression is an equality constraint check (==).
+    We check after the refinement if the new value of the variable is outside its integer bounds and if that is the case, either raise the exception "NotRefinable" or set it to bottom. *)
+module type ExtendedConvBounds =
+sig
+  include ConvBounds
+  val get_env: t -> Environment.t
+  val bot : unit -> t
+end
+module BoundsCheckMeetTcons (Bounds: ExtendedConvBounds) (V: SV) = struct
+  exception NotRefinable
+  module Convert = Convert (V) (Bounds) (struct let allow_global = true end) (Tracked)
+
+  let meet_tcons_one_var_eq res expr =
+    let overflow_res res = if IntDomain.should_ignore_overflow (Cilfacade.get_ikind_exp expr) then res else raise NotRefinable in
+    match Convert.find_one_var expr with
+    | None -> overflow_res res
+    | Some v ->
+      let ik = Cilfacade.get_ikind v.vtype in
+      match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res (Bounds.get_env res) (Lval (Cil.var v)) true) with
+      | Some _, Some _ when not (Cil.isSigned ik) -> raise NotRefinable 
+      | Some min, Some max ->
+        assert (Z.equal min max); (* other bounds impossible in affeq *)
+        let (min_ik, max_ik) = IntDomain.Size.range ik in
+        if Z.compare min min_ik < 0 || Z.compare max max_ik > 0 then
+          if IntDomain.should_ignore_overflow ik then Bounds.bot () else raise NotRefinable
+        else res
+      | exception Convert.Unsupported_CilExp _
+      | _, _ -> overflow_res res
+end

tests/regression/77-lin2vareq/11-overflow_ignored.c

@@ -0,0 +1,16 @@
+// SKIP PARAM: --set ana.activated[+] lin2vareq --set sem.int.signed_overflow assume_none
+
+#include <stdio.h>
+
+int main() {
+  int x;
+  int k;
+  int y;
+
+  x = k + 1;
+
+  __goblint_check(x == k + 1); // SUCCESS
+
+
+  return 0;
+}

tests/regression/77-lin2vareq/12-overflow.c

@@ -0,0 +1,23 @@
+// SKIP PARAM: --set ana.activated[+] lin2vareq  --enable ana.int.interval
+
+#include <stdio.h>
+
+int main() {
+  int x;
+  int k;
+  int y;
+
+  x = k + 1;
+  //there might be an overflow
+  __goblint_check(x == k + 1); // UNKNOWN!
+
+  int unknown;
+
+  if (unknown < 300 && unknown > 0) {
+    x = unknown;
+    // an overflow is not possible
+    __goblint_check(x == unknown); // SUCCESS
+  }
+
+  return 0;
+}

tests/regression/77-lin2vareq/13-bounds_guards_ov.c

@@ -0,0 +1,18 @@
+//SKIP PARAM: --set ana.activated[+] lin2vareq --set sem.int.signed_overflow assume_top --enable ana.int.interval
+// same test as 63-affeq/10-bounds_guards.ov.c
+int main() {
+    int x, y;
+    int p = 0;
+
+    if (x - 2 == __INT32_MAX__) {
+      __goblint_check(x == __INT32_MAX__ + 2); //UNKNOWN!
+      p = 1;
+    }
+
+    __goblint_check(p == 0); //UNKNOWN!
+
+    if (x + y == __INT32_MAX__) {
+        __goblint_check(1);
+    }
+
+}