From 2e50f2b5ff756e341ffb8d12b2390132a3e4fe5d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 11 Mar 2024 16:25:13 +0100 Subject: [PATCH] Fixes & Desiderata --- src/cdomains/apron/sharedFunctions.apron.ml | 67 +++++++++++-------- .../77-lin2vareq/31-unsigned-non-const.c | 16 +++++ tests/regression/77-lin2vareq/32-ahooga.c | 18 +++++ 3 files changed, 73 insertions(+), 28 deletions(-) create mode 100644 tests/regression/77-lin2vareq/31-unsigned-non-const.c create mode 100644 tests/regression/77-lin2vareq/32-ahooga.c diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 8470a2fffa..7b8360e7a5 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -80,38 +80,49 @@ struct | _ -> None (* for other exception *) ) - (** This still tries to establish bounds via Bounds.bound_texpr, which may be more precise in case ana.int.interval - is disabled and the relational analysis manages to evaluate a value to an interval, which can then not be represented - as the result of an EvalInt query. This is a workaround and works as long as only one relational domain is used. - With multiple domains and disabled interval domain, the queries will not be able to exchange interval information, - and each analysis will only be able to establish constant bounds, but only its own interval bounds and not interval bounds - established by other analyses.*) - let overflow_handling no_ov ik env expr d exp = - match Cilfacade.get_ikind_exp exp with - | exception Invalid_argument e -> raise (Unsupported_CilExp Exp_not_supported) (* expression is not an integer expression, i.e. float *) - | ik -> - if IntDomain.should_wrap ik || not (Lazy.force no_ov) then ( - let (type_min, type_max) = IntDomain.Size.range ik in - let texpr1 = Texpr1.of_expr env expr in - match Bounds.bound_texpr d texpr1 with - | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 -> - () - | min_opt, max_opt -> - if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)\n" CilType.Exp.pretty exp (Pretty.docOpt (IntOps.BigIntOps.pretty ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pretty ())) max_opt; - raise (Unsupported_CilExp Overflow) - ) let texpr1_expr_of_cil_exp (ask:Queries.ask) d env exp no_ov = let conv exp = + let module IDT = IntDomain.IntDomTuple in let query e ik = let res = match ask.f (EvalInt e) with | `Bot -> raise (Unsupported_CilExp Exp_not_supported) (* This should never happen according to Michael Schwarz *) - | `Top -> IntDomain.IntDomTuple.top_of ik - | `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) in - if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/query: %a -> %a\n" d_plainexp e IntDomain.IntDomTuple.pretty res; + | `Top -> + IDT.top_of ik + | `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) + in + if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/query: %a -> %a\n" d_plainexp e IDT.pretty res; res in + (** This still tries to establish bounds via Bounds.bound_texpr, which may be more precise in case ana.int.interval + is disabled and the relational analysis manages to evaluate a value to an interval, which can then not be represented + as the result of an EvalInt query. This is a workaround and works as long as only one relational domain is used. + With multiple domains and disabled interval domain, the queries will not be able to exchange interval information, + and each analysis will only be able to establish constant bounds, but only its own interval bounds and not interval bounds + established by other analyses.*) + let overflow_handling no_ov ik env expr d exp = + match Cilfacade.get_ikind_exp exp with + | exception Invalid_argument e -> raise (Unsupported_CilExp Exp_not_supported) (* expression is not an integer expression, i.e. float *) + | ik -> + if IntDomain.should_wrap ik || not (Lazy.force no_ov) then ( + let (type_min, type_max) = IntDomain.Size.range ik in + let texpr1 = Texpr1.of_expr env expr in + match Bounds.bound_texpr d texpr1 with + | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 -> + () + | min_opt, max_opt -> + (* Bounds did not manage to bound this, so we ask a query *) + let i = query exp ik in + match IDT.minimal i, IDT.maximal i with + | Some min, Some max when not (IDT.is_top_of ik (IDT.of_interval ~suppress_ovwarn:true ik (min, max))) -> + (* Checks that the interval information is not interval top. This works as we do not have dedicated wrap-around handling *) + () + | _ -> + if M.tracing then M.trace "relation" "may overflow: %a (%a, %a)\n" CilType.Exp.pretty exp (Pretty.docOpt (IntOps.BigIntOps.pretty ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pretty ())) max_opt; + raise (Unsupported_CilExp Overflow) + ) + in (* recurse without env and ask arguments *) let rec texpr1_expr_of_cil_exp = function | Lval (Var v, NoOffset) when Tracked.varinfo_tracked v -> @@ -140,8 +151,8 @@ struct let simplify e = let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) in let simp = query e ikind in - let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ikind simp in - if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a\n" d_plainexp e IntDomain.IntDomTuple.pretty simp; + let const = IDT.to_int @@ IDT.cast_to ikind simp in + if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a\n" d_plainexp e IDT.pretty simp; BatOption.map_default (fun c -> Const (CInt (c, ikind, None))) e const in let texpr1 e = texpr1_expr_of_cil_exp (simplify e) in @@ -162,14 +173,14 @@ struct (* try to evaluate e by EvalInt Query *) let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) in (* convert response to a constant *) - let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res in + let const = IDT.to_int @@ IDT.cast_to t_ik res in match const with | Some c -> Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z c))) (* Got a constant value -> use it straight away *) (* I gotten top, we can not guarantee injectivity *) - | None -> if IntDomain.IntDomTuple.is_top_of t_ik res then raise (Unsupported_CilExp (Cast_not_injective t)) + | None -> if IDT.is_top_of t_ik res then raise (Unsupported_CilExp (Cast_not_injective t)) else ( (* Got a ranged value different from top, so let's check bounds manually *) let (ik_min, ik_max) = IntDomain.Size.range t_ik in - match IntDomain.IntDomTuple.minimal res, IntDomain.IntDomTuple.maximal res with + match IDT.minimal res, IDT.maximal res with | Some min, Some max when min >= ik_min && max <= ik_max -> texpr1_expr_of_cil_exp e | _ -> raise (Unsupported_CilExp (Cast_not_injective t))) | exception Cilfacade.TypeOfError _ (* typeOf inner e, not outer exp *) diff --git a/tests/regression/77-lin2vareq/31-unsigned-non-const.c b/tests/regression/77-lin2vareq/31-unsigned-non-const.c new file mode 100644 index 0000000000..4c1fd2366b --- /dev/null +++ b/tests/regression/77-lin2vareq/31-unsigned-non-const.c @@ -0,0 +1,16 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --enable ana.int.interval +#include + +int main(void) { + int top; + unsigned int i = 0; + unsigned int j; + + if(top) { + i = 1; + } + + j = i+1; + + __goblint_check(j == i+1); +} diff --git a/tests/regression/77-lin2vareq/32-ahooga.c b/tests/regression/77-lin2vareq/32-ahooga.c new file mode 100644 index 0000000000..900a505823 --- /dev/null +++ b/tests/regression/77-lin2vareq/32-ahooga.c @@ -0,0 +1,18 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --enable ana.int.interval +#include +#include + +int main(void) { + int top; + unsigned int i = 2; + unsigned int j; + + if(top) { + i = 3; + } + + j = i + UINT_MAX; + + // Holds in the concrete + __goblint_check(j == i-1); //UNKNOWN +}