Skip to content

Commit

Permalink
Handle LNot for float in forward evaluation and refinement
Browse files Browse the repository at this point in the history
  • Loading branch information
michael-schwarz committed Jan 28, 2024
1 parent 6392583 commit 0cc39e2
Show file tree
Hide file tree
Showing 3 changed files with 55 additions and 14 deletions.
7 changes: 4 additions & 3 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
36 changes: 25 additions & 11 deletions src/analyses/baseInvariant.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
26 changes: 26 additions & 0 deletions tests/regression/57-floats/22-lnot.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
//PARAM: --enable ana.float.interval
#include<goblint.h>
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;
}

0 comments on commit 0cc39e2

Please sign in to comment.