From 2fb8604cb202b786efe29f9647c3ef8cd25fa0cc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Mar 2024 17:30:45 +0200 Subject: [PATCH 1/3] Replace option with polymorpic variant for base invariant fallback --- src/analyses/baseInvariant.ml | 46 +++++++++++++++++------------------ 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 7154768a75..fa3c069621 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -115,7 +115,7 @@ struct let invariant_fallback ctx st exp tv = (* We use a recursive helper function so that x != 0 is false can be handled * as x == 0 is true etc *) - let rec helper (op: binop) (lval: lval) (value: VD.t) (tv: bool): (lval * VD.t) option = + let rec helper (op: binop) (lval: lval) (value: VD.t) (tv: bool): [`Refine of lval * VD.t | `NotUnderstood] = match (op, lval, value, tv) with (* The true-branch where x == value: *) | Eq, x, value, true -> @@ -123,8 +123,8 @@ struct (match value with | Int n -> let ikind = Cilfacade.get_ikind_exp (Lval lval) in - Some (x, Int (ID.cast_to ikind n)) - | _ -> Some(x, value)) + `Refine (x, Int (ID.cast_to ikind n)) + | _ -> `Refine (x, value)) (* The false-branch for x == value: *) | Eq, x, value, false -> begin match value with @@ -134,26 +134,26 @@ struct (* When x != n, we can return a singleton exclusion set *) if M.tracing then M.tracec "invariant" "Yes, %a is not %a\n" d_lval x GobZ.pretty n; let ikind = Cilfacade.get_ikind_exp (Lval lval) in - Some (x, Int (ID.of_excl_list ikind [n])) - | None -> None + `Refine (x, Int (ID.of_excl_list ikind [n])) + | None -> `NotUnderstood end | Address n -> begin if M.tracing then M.tracec "invariant" "Yes, %a is not %a\n" d_lval x AD.pretty n; match eval_rv_address ~ctx st (Lval x) with | Address a when AD.is_definite n -> - Some (x, Address (AD.diff a n)) + `Refine (x, Address (AD.diff a n)) | Top when AD.is_null n -> - Some (x, Address AD.not_null) + `Refine (x, Address AD.not_null) | v -> if M.tracing then M.tracec "invariant" "No address invariant for: %a != %a\n" VD.pretty v AD.pretty n; - None + `NotUnderstood end - (* | Address a -> Some (x, value) *) + (* | Address a -> `Refine (x, value) *) | _ -> (* We can't say anything else, exclusion sets are finite, so not * being in one means an infinite number of values *) if M.tracing then M.tracec "invariant" "Failed! (not a definite value)\n"; - None + `NotUnderstood end | Ne, x, value, _ -> helper Eq x value (not tv) | Lt, x, value, _ -> begin @@ -166,10 +166,10 @@ struct match limit_from n with | Some n -> if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a\n\n" d_lval x GobZ.pretty n; - Some (x, Int (range_from n)) - | None -> None + `Refine (x, Int (range_from n)) + | None -> `NotUnderstood end - | _ -> None + | _ -> `NotUnderstood end | Le, x, value, _ -> begin match value with @@ -181,16 +181,16 @@ struct match limit_from n with | Some n -> if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a\n\n" d_lval x GobZ.pretty n; - Some (x, Int (range_from n)) - | None -> None + `Refine (x, Int (range_from n)) + | None -> `NotUnderstood end - | _ -> None + | _ -> `NotUnderstood end | Gt, x, value, _ -> helper Le x value (not tv) | Ge, x, value, _ -> helper Lt x value (not tv) | _ -> if M.tracing then M.trace "invariant" "Failed! (operation not supported)\n\n"; - None + `NotUnderstood in if M.tracing then M.traceli "invariant" "assume expression %a is %B\n" d_exp exp tv; let null_val (typ:typ):VD.t = @@ -199,7 +199,7 @@ struct | TEnum({ekind=_;_},_) | _ -> Int (ID.of_int (Cilfacade.get_ikind typ) Z.zero) in - let rec derived_invariant exp tv = + let rec derived_invariant exp tv: [`Refine of lval * VD.t | `NotUnderstood] = let switchedOp = function Lt -> Gt | Gt -> Lt | Le -> Ge | Ge -> Le | x -> x in (* a op b <=> b (switchedOp op) b *) match exp with (* Since we handle not only equalities, the order is important *) @@ -216,8 +216,8 @@ struct if VD.is_safe_cast t1 (Cilfacade.typeOfLval x) then derived_invariant (BinOp (op, Lval x, rval, typ)) tv else - None - | _ -> None) + `NotUnderstood + | _ -> `NotUnderstood) | BinOp(op, rval, CastE (TInt (_, _) as ti, Lval x), typ) -> derived_invariant (BinOp (switchedOp op, CastE(ti, Lval x), rval, typ)) tv (* Cases like if (x) are treated like if (x != 0) *) @@ -228,12 +228,12 @@ struct | UnOp (LNot,uexp,typ) -> derived_invariant uexp (not tv) | _ -> if M.tracing then M.tracec "invariant" "Failed! (expression %a not understood)\n\n" d_plainexp exp; - None + `NotUnderstood in match derived_invariant exp tv with - | Some (lval, value) -> + | `Refine (lval, value) -> refine_lv_fallback ctx st lval value tv - | None -> + | `NotUnderstood -> if M.tracing then M.traceu "invariant" "Doing nothing.\n"; M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_exp exp; st From 6f19d3d9f2fa032c9d46e00bbf7343233db90b5b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Mar 2024 17:46:30 +0200 Subject: [PATCH 2/3] Avoid base invariant fallback not understood message on reflexive pointer literal equality (closes #1374) --- src/analyses/baseInvariant.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index fa3c069621..3dceede426 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -115,7 +115,7 @@ struct let invariant_fallback ctx st exp tv = (* We use a recursive helper function so that x != 0 is false can be handled * as x == 0 is true etc *) - let rec helper (op: binop) (lval: lval) (value: VD.t) (tv: bool): [`Refine of lval * VD.t | `NotUnderstood] = + let rec helper (op: binop) (lval: lval) (value: VD.t) (tv: bool): [> `Refine of lval * VD.t | `NotUnderstood] = match (op, lval, value, tv) with (* The true-branch where x == value: *) | Eq, x, value, true -> @@ -199,7 +199,7 @@ struct | TEnum({ekind=_;_},_) | _ -> Int (ID.of_int (Cilfacade.get_ikind typ) Z.zero) in - let rec derived_invariant exp tv: [`Refine of lval * VD.t | `NotUnderstood] = + let rec derived_invariant exp tv: [`Refine of lval * VD.t | `NothingToRefine | `NotUnderstood] = let switchedOp = function Lt -> Gt | Gt -> Lt | Le -> Ge | Ge -> Le | x -> x in (* a op b <=> b (switchedOp op) b *) match exp with (* Since we handle not only equalities, the order is important *) @@ -220,6 +220,9 @@ struct | _ -> `NotUnderstood) | BinOp(op, rval, CastE (TInt (_, _) as ti, Lval x), typ) -> derived_invariant (BinOp (switchedOp op, CastE(ti, Lval x), rval, typ)) tv + | BinOp(op, (Const _ | AddrOf _), rval, typ) -> + (* This is last such that we never reach here with rval being Lval (it is swapped around). *) + `NothingToRefine (* Cases like if (x) are treated like if (x != 0) *) | Lval x -> (* There are two correct ways of doing it: "if ((int)x != 0)" or "if (x != (typeof(x))0))" @@ -233,6 +236,9 @@ struct match derived_invariant exp tv with | `Refine (lval, value) -> refine_lv_fallback ctx st lval value tv + | `NothingToRefine -> + if M.tracing then M.traceu "invariant" "Doing to refine.\n"; + st | `NotUnderstood -> if M.tracing then M.traceu "invariant" "Doing nothing.\n"; M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_exp exp; From 6ac23e3277bbd9069170a66ce714e1aed80266bf Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Mar 2024 18:42:17 +0200 Subject: [PATCH 3/3] Fix tracing message when nothing to refine Co-authored-by: Michael Schwarz --- src/analyses/baseInvariant.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 3dceede426..42e3a3fd48 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -237,7 +237,7 @@ struct | `Refine (lval, value) -> refine_lv_fallback ctx st lval value tv | `NothingToRefine -> - if M.tracing then M.traceu "invariant" "Doing to refine.\n"; + if M.tracing then M.traceu "invariant" "Nothing to refine.\n"; st | `NotUnderstood -> if M.tracing then M.traceu "invariant" "Doing nothing.\n";