From 0cc39e2a3c60148b9339313e85d0e222dd1e22e0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 28 Jan 2024 19:12:55 +0100 Subject: [PATCH 1/3] Handle LNot for float in forward evaluation and refinement --- src/analyses/base.ml | 7 +++--- src/analyses/baseInvariant.ml | 36 +++++++++++++++++++--------- tests/regression/57-floats/22-lnot.c | 26 ++++++++++++++++++++ 3 files changed, 55 insertions(+), 14 deletions(-) create mode 100644 tests/regression/57-floats/22-lnot.c diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 42e43b623a..28e5d87c50 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -178,14 +178,15 @@ struct | LNot -> ID.lognot let unop_FD = function - | Neg -> FD.neg + | Neg -> (fun v -> (Float (FD.neg v):value)) + | LNot -> (fun c -> Int (FD.eq c (FD.of_const (FD.get_fkind c) 0.))) (* other unary operators are not implemented on float values *) - | _ -> (fun c -> FD.top_of (FD.get_fkind c)) + | _ -> (fun c -> Float (FD.top_of (FD.get_fkind c))) (* Evaluating Cil's unary operators. *) let evalunop op typ: value -> value = function | Int v1 -> Int (ID.cast_to (Cilfacade.get_ikind typ) (unop_ID op v1)) - | Float v -> Float (unop_FD op v) + | Float v -> unop_FD op v | Address a when op = LNot -> if AD.is_null a then Int (ID.of_bool (Cilfacade.get_ikind typ) true) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index e66a431ccf..7a3d5de806 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -568,17 +568,31 @@ struct else match exp, c_typed with | UnOp (LNot, e, _), Int c -> - let ikind = Cilfacade.get_ikind_exp e in - let c' = - match ID.to_bool (unop_ID LNot c) with - | Some true -> - (* i.e. e should evaluate to [1,1] *) - (* LNot x is 0 for any x != 0 *) - ID.of_excl_list ikind [BI.zero] - | Some false -> ID.of_bool ikind false - | _ -> ID.top_of ikind - in - inv_exp (Int c') e st + (match Cilfacade.typeOf e with + | TInt _ | TPtr _ -> + let ikind = Cilfacade.get_ikind_exp e in + let c' = + match ID.to_bool (unop_ID LNot c) with + | Some true -> + (* i.e. e should evaluate to [1,1] *) + (* LNot x is 0 for any x != 0 *) + ID.of_excl_list ikind [BI.zero] + | Some false -> ID.of_bool ikind false + | _ -> ID.top_of ikind + in + inv_exp (Int c') e st + | TFloat(fkind, _) when ID.to_bool (unop_ID LNot c) = Some false -> + (* C99 ยง6.5.3.3/5 *) + (* The result of the logical negation operator ! is 0 if the value of its operand compares *) + (* unequal to 0, 1 if the value of its operand compares equal to 0. The result has type int. *) + (* The expression !E is equivalent to (0==E). *) + (* NaN compares unequal to 0 so no problems *) + (* We do not have exclusions for floats, so we do not bother here with the other case *) + let zero_float = FD.of_const fkind 0. in + inv_exp (Float zero_float) e st + | _ -> st + + ) | UnOp (Neg, e, _), Float c -> inv_exp (Float (unop_FD Neg c)) e st | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *) diff --git a/tests/regression/57-floats/22-lnot.c b/tests/regression/57-floats/22-lnot.c new file mode 100644 index 0000000000..5c043e4ead --- /dev/null +++ b/tests/regression/57-floats/22-lnot.c @@ -0,0 +1,26 @@ +//PARAM: --enable ana.float.interval +#include +int main() { + float x = 0.0f; + int z = !x; + + int reach; + + if(z) { + __goblint_check(1); //Reachable + reach = 1; + } else { + reach = 0; + } + + __goblint_check(reach == 1); + + float y; + if (!y) { + __goblint_check(y == 0.0f); + } else { + __goblint_check(1); //Reachable + } + + return 0; +} \ No newline at end of file From 9f0c940f17c354515f9d41465cc3fbd0de8875c3 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 4 Feb 2024 11:07:16 +0100 Subject: [PATCH 2/3] unop_FD: Handle `BNot` explicitely --- src/analyses/base.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 77394a52cd..383c76fad8 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -179,8 +179,8 @@ struct let unop_FD = function | Neg -> (fun v -> (Float (FD.neg v):value)) | LNot -> (fun c -> Int (FD.eq c (FD.of_const (FD.get_fkind c) 0.))) - (* other unary operators are not implemented on float values *) - | _ -> (fun c -> Float (FD.top_of (FD.get_fkind c))) + | BNot -> failwith "BNot on a value of type float!" + (* Evaluating Cil's unary operators. *) let evalunop op typ: value -> value = function From c8b2fb7f30357a1efce80df5cba00022f45b74d2 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 4 Feb 2024 11:08:55 +0100 Subject: [PATCH 3/3] Share `eval_unop` definitions between `base.ml` and `baseInvariant.ml` --- src/analyses/base.ml | 6 ++++++ src/analyses/baseInvariant.ml | 15 ++++----------- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 383c76fad8..63c2879a9a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1645,6 +1645,9 @@ struct module V = V module G = G + let unop_ID = unop_ID + let unop_FD = unop_FD + let eval_rv = eval_rv let eval_rv_address = eval_rv_address let eval_lv = eval_lv @@ -2842,6 +2845,9 @@ struct let ost = octx.local + let unop_ID = unop_ID + let unop_FD = unop_FD + (* all evals happen in octx with non-top values *) let eval_rv ~ctx st e = eval_rv ~ctx:octx ost e let eval_rv_address ~ctx st e = eval_rv_address ~ctx:octx ost e diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 08ec012c10..7154768a75 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -14,6 +14,9 @@ sig module V: Analyses.SpecSysVar module G: Lattice.S + val unop_ID: Cil.unop -> ID.t -> ID.t + val unop_FD: Cil.unop -> FD.t -> VD.t + val eval_rv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t val eval_rv_address: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> exp -> VD.t val eval_lv: ctx:(D.t, G.t, _, V.t) Analyses.ctx -> D.t -> lval -> AD.t @@ -41,16 +44,6 @@ module Make (Eval: Eval) = struct open Eval - let unop_ID = function - | Neg -> ID.neg - | BNot -> ID.lognot - | LNot -> ID.c_lognot - - let unop_FD = function - | Neg -> FD.neg - (* other unary operators are not implemented on float values *) - | _ -> (fun c -> FD.top_of (FD.get_fkind c)) - let is_some_bot (x:VD.t) = match x with | Bot -> false (* HACK: bot is here due to typing conflict (we do not cast appropriately) *) @@ -589,7 +582,7 @@ struct inv_exp (Float zero_float) e st | _ -> st ) - | UnOp (Neg, e, _), Float c -> inv_exp (Float (unop_FD Neg c)) e st + | UnOp (Neg, e, _), Float c -> inv_exp (unop_FD Neg c) e st | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *) | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_safe_cast t2 (Cilfacade.typeOf e2) ->