From 6d84ca4a96e6592b47c880ee207a55048be67cfb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Mar 2024 13:00:30 +0200 Subject: [PATCH] Refine addresses generally in base (issue #1374) --- src/analyses/base.ml | 2 ++ src/analyses/baseInvariant.ml | 39 +++++++++++++++++++++++++++++++++-- 2 files changed, 39 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 9aca9e2079..f8610671c8 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1680,6 +1680,7 @@ struct let id_meet_down ~old ~c = ID.meet old c let fd_meet_down ~old ~c = FD.meet old c + let ad_meet_down ~old ~c = AD.meet old c let contra _ = raise Deadcode end @@ -2886,6 +2887,7 @@ struct (* don't meet with current octx values when propagating inverse operands down *) let id_meet_down ~old ~c = c let fd_meet_down ~old ~c = c + let ad_meet_down ~old ~c = c let contra st = st end diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 7154768a75..cbfebc20b3 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -32,6 +32,7 @@ sig val id_meet_down: old:ID.t -> c:ID.t -> ID.t val fd_meet_down: old:FD.t -> c:FD.t -> FD.t + val ad_meet_down: old:AD.t -> c:AD.t -> AD.t (** Handle contradiction. @@ -416,6 +417,34 @@ struct if M.tracing then M.tracel "inv" "Unhandled operator %a\n" d_binop op; a, b in + let inv_bin_addr (a, b) c op = + let meet_bin a' b' = ad_meet_down ~old:a ~c:a', ad_meet_down ~old:b ~c:b' in + match op with + | Eq | Ne as op -> + begin match op, ID.to_bool c with + | Eq, Some true + | Ne, Some false -> (* def. equal: if they compare equal, both values must be from the meet *) + (ad_meet_down ~old:a ~c:b, ad_meet_down ~old:b ~c:a) + | Eq, Some false + | Ne, Some true -> (* def. unequal *) + (* Both values can not be in the meet together, but it's not sound to exclude the meet from both. + * e.g. a=[0,1], b=[1,2], meet a b = [1,1], but (a != b) does not imply a=[0,0], b=[2,2] since others are possible: a=[1,1], b=[2,2] + * Only if a is a definite value, we can exclude it from b: *) + (* Used to cause inconsistent results: + interval not sufficiently refined: + inv_bin_int: unequal: (Unknown int([-31,31]),[0,1]) and (0,[0,0]); ikind: int; a': (Not {0}([-31,31]),[-2147483648,2147483647]), b': (0,[0,0]) + binop: m == 0, a': (Not {0}([-31,31]),[0,1]), b': (0,[0,0]) *) + let excl a b = b in + let a' = excl b a in + let b' = excl a b in + if M.tracing then M.tracel "inv" "inv_bin_addr: unequal: %a and %a; a': %a, b': %a\n" AD.pretty a AD.pretty b AD.pretty a' AD.pretty b'; + meet_bin a' b' + | _, _ -> a, b + end + | op -> + if M.tracing then M.tracel "inv" "Unhandled operator %a\n" d_binop op; + a, b + in let inv_bin_float (a, b) c op = let open Stdlib in let meet_bin a' b' = fd_meet_down ~old:a ~c:a', fd_meet_down ~old:b ~c:b' in @@ -691,7 +720,13 @@ struct st'' (* Mixed Float and Int cases should never happen, as there are no binary operators with one float and one int parameter ?!*) | Int _, Float _ | Float _, Int _ -> failwith "ill-typed program"; - (* | Address a, Address b -> ... *) + | Address a, Address b -> + let ikres = Cilfacade.get_ikind_exp e in (* might be different from argument types, e.g. for LT, GT, EQ, ... *) + let a', b' = inv_bin_addr (a, b) (c_int ikres) op in + if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e ID.pretty (c_int ikres) AD.pretty a' AD.pretty b'; + let st' = inv_exp (Address a') e1 st in + let st'' = inv_exp (Address b') e2 st' in + st'' | 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 @@ -772,7 +807,7 @@ struct update_lval c x c' AD.pretty | _ -> assert false end - | Const _ , _ -> st (* nothing to do *) + | (Const _| AddrOf _) , _ -> st (* nothing to do *) | CastE ((TFloat (_, _)), e), Float c -> (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with | TFloat (FLongDouble as fk, _), FFloat