From 526e8e4ee0e5708d2029c39e8fe9ea6148425c2a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 10 Sep 2023 13:53:37 +0200 Subject: [PATCH] Handle `bitand` in intervals and def_exc; Add test --- src/analyses/baseInvariant.ml | 26 ++++++++++---- src/cdomains/intDomain.ml | 36 +++++++++++++++++-- tests/regression/37-congruence/13-bitand.c | 41 ++++++++++++++++++++++ 3 files changed, 94 insertions(+), 9 deletions(-) create mode 100644 tests/regression/37-congruence/13-bitand.c diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 096d50b89be..70c6ed9101f 100644 --- a/src/analyses/baseInvariant.ml +++ b/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 diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index c78e66e2bfb..312f5d7540e 100644 --- a/src/cdomains/intDomain.ml +++ b/src/cdomains/intDomain.ml @@ -826,7 +826,18 @@ 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.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 = @@ -2282,7 +2293,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 diff --git a/tests/regression/37-congruence/13-bitand.c b/tests/regression/37-congruence/13-bitand.c new file mode 100644 index 00000000000..b6320690142 --- /dev/null +++ b/tests/regression/37-congruence/13-bitand.c @@ -0,0 +1,41 @@ +// PARAM: --enable ana.int.congruence --set sem.int.signed_overflow assume_none +#include + +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 + + // For some reason does not work for longs yet + 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); +}