Merge pull request #1154 from goblint/issue_1153

Handle some special cases of `bitand` in `invariant` and `Interval`, `DefExc`, and `Congruences`

src/analyses/baseInvariant.ml

@@ -410,6 +410,18 @@ struct
           meet_bin c c
         else
           a, b
+      | BAnd as op ->
+        (* we only attempt to refine a here *)
+        let a =
+          match ID.to_int b with
+          | Some x when BI.equal x BI.one ->
+            (match ID.to_bool c with
+             | Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2))
+             | Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2))
+             | None -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a 1 = %a\n" d_binop op ID.pretty c; a)
+          | _ -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a %a = %a\n" d_binop op ID.pretty b ID.pretty c; a
+        in
+        a, b
       | op ->
         if M.tracing then M.tracel "inv" "Unhandled operator %a\n" d_binop op;
         a, b
@@ -545,8 +557,8 @@ struct
     in
     let eval e st = eval_rv a gs st e in
     let eval_bool e st = match eval e st with Int i -> ID.to_bool i | _ -> None in
-    let unroll_fk_of_exp e = 
-      match unrollType (Cilfacade.typeOf e) with 
+    let unroll_fk_of_exp e =
+      match unrollType (Cilfacade.typeOf e) with
       | TFloat (fk, _) -> fk
       | _ -> failwith "value which was expected to be a float is of different type?!"
     in
@@ -700,8 +712,8 @@ struct
               begin match t with
                 | TInt (ik, _) ->
                   begin match x with
-                    | ((Var v), offs) -> 
-                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); 
+                    | ((Var v), offs) ->
+                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       let tv_opt = ID.to_bool c in
                       begin match tv_opt with
                         | Some tv ->
@@ -735,12 +747,12 @@ struct
               begin match t with
                 | TFloat (fk, _) ->
                   begin match x with
-                    | ((Var v), offs) -> 
-                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); 
+                    | ((Var v), offs) ->
+                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
                         | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
                         | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st
-                        | `Lifted (Fabs (ret_fk, xFloat)) -> 
+                        | `Lifted (Fabs (ret_fk, xFloat)) ->
                           let inv = FD.inv_fabs (FD.cast_to ret_fk c) in
                           if FD.is_bot inv then
                             raise Analyses.Deadcode

src/cdomains/intDomain.ml

@@ -514,7 +514,7 @@ module Size = struct (* size in bits as int, range as int64 *)
 
   let cast t x = (* TODO: overflow is implementation-dependent! *)
     if t = IBool then
-      (* C11 6.3.1.2 Boolean type *) 
+      (* C11 6.3.1.2 Boolean type *)
       if Z.equal x Z.zero then Z.zero else Z.one
     else
       let a,b = range t in
@@ -826,7 +826,19 @@ struct
       | _              -> (top_of ik,{underflow=true; overflow=true})
 
   let bitxor = bit (fun _ik -> Ints_t.bitxor)
-  let bitand = bit (fun _ik -> Ints_t.bitand)
+
+  let bitand ik i1 i2 =
+    match is_bot i1, is_bot i2 with
+    | true, true -> bot_of ik
+    | true, _
+    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show i1) (show i2)))
+    | _ ->
+      match to_int i1, to_int i2 with
+      | Some x, Some y -> (try of_int ik (Ints_t.bitand x y) |> fst with Division_by_zero -> top_of ik)
+      | _, Some y when Ints_t.equal y Ints_t.zero -> of_int ik Ints_t.zero |> fst
+      | _, Some y when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst
+      | _ -> top_of ik
+
   let bitor  = bit (fun _ik -> Ints_t.bitor)
 
   let bit1 f ik i1 =
@@ -1978,15 +1990,15 @@ struct
   let top_of ik = `Excluded (S.empty (), size ik)
   let cast_to ?torg ?no_ov ik = function
     | `Excluded (s,r) ->
-      let r' = size ik in 
+      let r' = size ik in
         if R.leq r r' then (* upcast -> no change *)
           `Excluded (s, r)
         else if ik = IBool then (* downcast to bool *)
           if S.mem BI.zero s then
             `Definite (BI.one)
           else
             `Excluded (S.empty(), r')
-        else 
+        else
           (* downcast: may overflow *)
           (* let s' = S.map (BigInt.cast_to ik) s in *)
           (* We want to filter out all i in s' where (t)x with x in r could be i. *)
@@ -2282,7 +2294,28 @@ struct
   let ge ik x y = le ik y x
 
   let bitnot = lift1 BigInt.bitnot
-  let bitand = lift2 BigInt.bitand
+
+  let bitand ik x y = norm ik (match x,y with
+      (* We don't bother with exclusion sets: *)
+      | `Excluded _, `Definite i ->
+        (* Except in two special cases *)
+        if BigInt.equal i BigInt.zero then
+          `Definite BigInt.zero
+        else if BigInt.equal i BigInt.one then
+          of_interval IBool (BigInt.zero, BigInt.one)
+        else
+          top ()
+      | `Definite _, `Excluded _
+      | `Excluded _, `Excluded _ -> top ()
+      (* The good case: *)
+      | `Definite x, `Definite y ->
+        (try `Definite (BigInt.bitand x y) with | Division_by_zero -> top ())
+      | `Bot, `Bot -> `Bot
+      | _ ->
+        (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
+        raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
+
+
   let bitor  = lift2 BigInt.bitor
   let bitxor = lift2 BigInt.bitxor
 
@@ -3134,7 +3167,7 @@ struct
 
   (** The implementation of the bit operations could be improved based on the master’s thesis
       'Abstract Interpretation and Abstract Domains' written by Stefan Bygde.
-      see: https://www.dsi.unive.it/~avp/domains.pdf *)
+      see: http://www.es.mdh.se/pdf_publications/948.pdf *)
   let bit2 f ik x y = match x, y with
     | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
@@ -3144,7 +3177,19 @@ struct
 
   let bitor ik x y = bit2 Ints_t.bitor ik x y
 
-  let bitand ik x y = bit2 Ints_t.bitand ik x y
+  let bitand ik x y =  match x, y with
+    | None, None -> None
+    | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
+    | Some (c, m), Some (c', m') ->
+      if (m =: Ints_t.zero && m' =: Ints_t.zero) then
+        (* both arguments constant *)
+        Some (Ints_t.bitand c c', Ints_t.zero)
+      else if m' =: Ints_t.zero && c' =: Ints_t.one && Ints_t.rem m (Ints_t.of_int 2) =: Ints_t.zero then
+        (* x & 1  and  x == c (mod 2*z) *)
+        (* Value is equal to LSB of c *)
+        Some (Ints_t.bitand c c', Ints_t.zero)
+      else
+        top ()
 
   let bitxor ik x y = bit2 Ints_t.bitxor ik x y
 

tests/regression/37-congruence/13-bitand.c

@@ -0,0 +1,40 @@
+// PARAM: --enable ana.int.congruence --set sem.int.signed_overflow assume_none
+#include <goblint.h>
+
+int main()
+{
+	// Assuming modulo expression
+
+	long x;
+	__goblint_assume(x % 2 == 1);
+	__goblint_check(x % 2 == 1);
+	__goblint_check(x & 1);
+
+	long y;
+	__goblint_assume(y % 2 == 0);
+	__goblint_check(y % 2 == 0);
+	__goblint_check(y & 1); //FAIL
+
+	long z;
+	__goblint_check(z & 1); //UNKNOWN!
+	__goblint_assume(z % 8 == 1);
+	__goblint_check(z & 1);
+
+	long xz;
+	__goblint_assume(xz % 3 == 1);
+	__goblint_check(xz & 1); //UNKNOWN!
+	__goblint_assume(xz % 6 == 1);
+	__goblint_check(xz & 1);
+
+	// Assuming bitwise expression
+
+	long a;
+	__goblint_assume(a & 1);
+	__goblint_check(a % 2 == 1);
+	__goblint_check(a & 1);
+
+	int b;
+	__goblint_assume(b & 1);
+	__goblint_check(b % 2 == 1);
+	__goblint_check(b & 1);
+}