Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Avoid base invariant fallback not understood message on reflexive pointer literal equality #1396

Merged
merged 4 commits into from
Apr 4, 2024
+29 −23
Merged

Avoid base invariant fallback not understood message on reflexive pointer literal equality #1396

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2fb8604
Replace option with polymorpic variant for base invariant fallback
sim642 Mar 21, 2024
6f19d3d
Avoid base invariant fallback not understood message on reflexive poi…
sim642 Mar 21, 2024
6ac23e3
Fix tracing message when nothing to refine
sim642 Mar 21, 2024
0c72199
Merge branch 'master' into issue-1374-2
michael-schwarz Mar 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 29 additions & 23 deletions src/analyses/baseInvariant.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,16 +115,16 @@ 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 ->
if M.tracing then M.tracec "invariant" "Yes, %a equals %a" d_lval x VD.pretty value;
(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
Expand All @@ -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" 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" 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" 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)";
None
`NotUnderstood
end
| Ne, x, value, _ -> helper Eq x value (not tv)
| Lt, x, value, _ -> begin
Expand All @@ -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" 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
Expand All @@ -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" 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)";
None
`NotUnderstood
in
if M.tracing then M.traceli "invariant" "assume expression %a is %B" d_exp exp tv;
let null_val (typ:typ):VD.t =
Expand All @@ -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 | `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 *)
Expand All @@ -216,10 +216,13 @@ 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
| 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))"
Expand All @@ -228,12 +231,15 @@ struct
| UnOp (LNot,uexp,typ) -> derived_invariant uexp (not tv)
| _ ->
if M.tracing then M.tracec "invariant" "Failed! (expression %a not understood)" 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 ->
| `NothingToRefine ->
if M.tracing then M.traceu "invariant" "Nothing to refine.";
st
| `NotUnderstood ->
if M.tracing then M.traceu "invariant" "Doing nothing.";
M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_exp exp;
st
Expand Down
Loading