Skip to content

Deduplicate C logical operators from int domains #1963

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

Draft
sim642 wants to merge 1 commit into
base: int-predicates
Choose a base branch
from
Draft

Deduplicate C logical operators from int domains #1963

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
19 changes: 15 additions & 4 deletions src/analyses/base.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,6 +174,17 @@ struct
| Some b -> ID.of_bool result_ik b
| None -> ID.of_interval result_ik (Z.zero, Z.one)

let id_unary_log = function
| Some b -> ID.of_bool IInt b
| None -> ID.top_of IInt (* TODO: [0,1] interval instead? *)

let id_binary_log f ~annihilator ik i1 i2 =
match ID.to_bool i1, ID.to_bool i2 with
| Some x, _ when x = annihilator -> ID.of_bool ik annihilator
| _, Some y when y = annihilator -> ID.of_bool ik annihilator
| Some x, Some y -> ID.of_bool ik (f x y)
| _ -> ID.top_of ik (* TODO: [0,1] interval instead? *)

(** Unary float predicates return non-zero for [true].
@see C11 7.12.3 *)
let fd_unary_pred = function
Expand All @@ -190,7 +201,7 @@ struct
let unop_ID = function
| Neg -> ID.neg
| BNot -> ID.lognot
| LNot -> ID.c_lognot
| LNot -> (fun x-> id_unary_log (Option.map not (ID.to_bool x)))

let unop_FD = function
| Neg -> (fun v -> (Float (FD.neg v):value))
Expand Down Expand Up @@ -256,8 +267,8 @@ struct
| BXor -> ID.logxor
| Shiftlt -> ID.shift_left
| Shiftrt -> ID.shift_right
| LAnd -> ID.c_logand
| LOr -> ID.c_logor
| LAnd -> id_binary_log (&&) ~annihilator:false result_ik
| LOr -> id_binary_log (||) ~annihilator:true result_ik
| b -> (fun x y -> (ID.top_of result_ik))

let binop_FD (result_fk: Cil.fkind) = function
Expand Down Expand Up @@ -2695,7 +2706,7 @@ struct
| Isgreaterequal (x,y) -> Int(fd_binary_pred (apply_binary FDouble FD.ge x y))
| Isless (x,y) -> Int(fd_binary_pred (apply_binary FDouble FD.lt x y))
| Islessequal (x,y) -> Int(fd_binary_pred (apply_binary FDouble FD.le x y))
| Islessgreater (x,y) -> Int(ID.c_logor (fd_binary_pred (apply_binary FDouble FD.lt x y)) (fd_binary_pred (apply_binary FDouble FD.gt x y)))
| Islessgreater (x,y) -> Int(id_binary_log (||) ~annihilator:true IInt (fd_binary_pred (apply_binary FDouble FD.lt x y)) (fd_binary_pred (apply_binary FDouble FD.gt x y))) (* TODO: avoid intermediate ID conversions *)
| Isunordered (x,y) -> Int(fd_binary_pred (apply_binary FDouble FD.unordered x y))
| Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
| Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
Expand Down
19 changes: 0 additions & 19 deletions src/cdomain/value/cdomains/int/bitfieldDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -397,25 +397,6 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
norm ik (z,o)
else top_of ik

(* Logic *)

let log1 f ik i1 = match to_bool i1 with
| None -> top_of ik
| Some x -> of_bool ik (f x)

let log2 f ~annihilator ik i1 i2 = match to_bool i1, to_bool i2 with
| Some x, _ when x = annihilator -> of_bool ik annihilator
| _, Some y when y = annihilator -> of_bool ik annihilator
| Some x, Some y -> of_bool ik (f x y)
| _ -> top_of ik

let c_logor = log2 (||) ~annihilator:true

let c_logand = log2 (&&) ~annihilator:false

let c_lognot ik i1 = log1 not ik i1


(* Bitwise *)

let logxor ik i1 i2 = BArith.logxor i1 i2 |> norm ik
Expand Down
23 changes: 0 additions & 23 deletions src/cdomain/value/cdomains/int/congruenceDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -205,29 +205,6 @@ struct

let narrow = meet

let log f ik i1 i2 =
match is_bot i1, is_bot i2 with
| true, true -> bot_of ik
| true, _
| _ , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show i1) (show i2)))
| _ ->
match to_bool i1, to_bool i2 with
| Some x, Some y -> of_bool ik (f x y)
| _ -> top_of ik

let c_logor = log (||)
let c_logand = log (&&)

let log1 f ik i1 =
if is_bot i1 then
bot_of ik
else
match to_bool i1 with
| Some x -> of_bool ik (f ik x)
| _ -> top_of ik

let c_lognot = log1 (fun _ik -> not)

let shift_right _ _ _ = top()

let shift_right ik x y =
Expand Down
16 changes: 0 additions & 16 deletions src/cdomain/value/cdomains/int/defExcDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -561,22 +561,6 @@ struct

let shift_right =
shift Z.shift_right
(* TODO: lift does not treat Not {0} as true. *)
let c_logand ik x y =
match to_bool x, to_bool y with
| Some false, _
| _, Some false ->
of_bool ik false
| _, _ ->
lift2 IntOps.BigIntOps.c_logand ik x y
let c_logor ik x y =
match to_bool x, to_bool y with
| Some true, _
| _, Some true ->
of_bool ik true
| _, _ ->
lift2 IntOps.BigIntOps.c_logor ik x y
let c_lognot ik x = match eq ik (of_int ik Z.zero) x with None -> top_of IInt | Some x -> of_bool IInt x (* TODO: avoid conversion *)

let invariant_ikind e ik (x:t) =
match x with
Expand Down
12 changes: 1 addition & 11 deletions src/cdomain/value/cdomains/int/enumsDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -373,16 +373,6 @@ module Enums : S with type int_t = Z.t = struct
let l_ik,_ = Size.range ikind in
of_interval ikind (l_ik, x)

let c_lognot ik x =
if is_bot x
then x
else
match to_bool x with
| Some b -> of_bool ik (not b)
| None -> top_bool

let c_logand = lift2 IntOps.BigIntOps.c_logand
let c_logor = lift2 IntOps.BigIntOps.c_logor
let maximal = function
| Inc xs when not (BISet.is_empty xs) -> Some (BISet.max_elt xs)
| Exc (excl,r) ->
Expand Down Expand Up @@ -436,7 +426,7 @@ module Enums : S with type int_t = Z.t = struct
else
None)

let ne ik x y = to_bool (c_lognot ik (match eq ik x y with None -> top_bool | Some x -> of_bool ik x)) (* TODO: avoid conversion *)
let ne ik x y = Option.map not (eq ik x y)

let invariant_ikind e ik x =
match x with
Expand Down
9 changes: 0 additions & 9 deletions src/cdomain/value/cdomains/int/intDomTuple.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -362,9 +362,6 @@ module IntDomTupleImpl = struct
let lognot ik =
map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.lognot ik)}

let c_lognot ik =
map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_lognot ik)}

let cast_to ?(suppress_ovwarn=false) ~kind ?from_ik ?no_ov t =
mapovc ~suppress_ovwarn ~op:(Cast kind) t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ~kind ?from_ik ?no_ov t)}

Expand Down Expand Up @@ -490,12 +487,6 @@ module IntDomTupleImpl = struct
let shift_right ik =
map2ovc ~op:(Binop Shiftrt) ik {f2_ovc= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.shift_right ik)}

let c_logand ik =
map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_logand ik)}

let c_logor ik =
map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_logor ik)}


(* printing boilerplate *)
let pretty_diff () (x,y) = dprintf "%a instead of %a" pretty x pretty y
Expand Down
25 changes: 0 additions & 25 deletions src/cdomain/value/cdomains/int/intervalDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,31 +180,6 @@ struct
else
narrow ik x y

let log f ~annihilator ik i1 i2 =
match is_bot i1, is_bot i2 with
| true, true -> bot_of ik
| true, _
| _ , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show i1) (show i2)))
| _ ->
match to_bool i1, to_bool i2 with
| Some x, _ when x = annihilator -> of_bool ik annihilator
| _, Some y when y = annihilator -> of_bool ik annihilator
| Some x, Some y -> of_bool ik (f x y)
| _ -> top_of ik

let c_logor = log (||) ~annihilator:true
let c_logand = log (&&) ~annihilator:false

let log1 f ik i1 =
if is_bot i1 then
bot_of ik
else
match to_bool i1 with
| Some x -> of_bool ik (f ik x)
| _ -> top_of ik

let c_lognot = log1 (fun _ik -> not)

let bit f ik i1 i2 =
match is_bot i1, is_bot i2 with
| true, true -> bot_of ik
Expand Down
22 changes: 0 additions & 22 deletions src/cdomain/value/cdomains/int/intervalSetDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -304,11 +304,6 @@ struct
let interval_to_int i = Interval.to_int (Some i)
let interval_to_bool i = Interval.to_bool (Some i)

let log f ik i1 i2 =
match (interval_to_bool i1, interval_to_bool i2) with
| Some x, Some y -> of_bool ik (f x y)
| _ -> top_of ik


let bit f ik (i1, i2) =
match (interval_to_int i1), (interval_to_int i2) with
Expand Down Expand Up @@ -435,23 +430,6 @@ struct

let shift_right ik x y = binary_op_with_ovc x y (interval_shiftright ik)

let c_lognot ik x =
let log1 f ik i1 =
match interval_to_bool i1 with
| Some x -> of_bool ik (f x)
| _ -> top_of ik
in
let interval_lognot = log1 not ik in
unop x interval_lognot

let c_logand ik x y =
let interval_logand = log (&&) ik in
binop x y interval_logand

let c_logor ik x y =
let interval_logor = log (||) ik in
binop x y interval_logor

let add ?no_ov = binary_op_with_norm IArith.add
let sub ?no_ov = binary_op_with_norm IArith.sub
let mul ?no_ov = binary_op_with_norm IArith.mul
Expand Down
14 changes: 0 additions & 14 deletions src/cdomain/value/cdomains/intDomain0.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -178,8 +178,6 @@ struct
(* Helper functions *)
let check_ikinds x y = if x.ikind <> y.ikind then raise (IncompatibleIKinds (GobPretty.sprintf "ikinds %a and %a are incompatible. Values: %a and %a" CilType.Ikind.pretty x.ikind CilType.Ikind.pretty y.ikind I.pretty x.v I.pretty y.v))
let lift op x = {x with v = op x.ikind x.v }
(* For logical operations the result is of type int *)
let lift_logical op x = {v = op x.ikind x.v; ikind = Cil.IInt}
let lift2 op x y = check_ikinds x y; {x with v = op x.ikind x.v y.v }
let lift2_cmp op x y = check_ikinds x y; op x.ikind x.v y.v

Expand Down Expand Up @@ -259,9 +257,6 @@ struct
let logxor = lift2 I.logxor
let shift_left x y = {x with v = I.shift_left x.ikind x.v y.v } (* TODO check ikinds*)
let shift_right x y = {x with v = I.shift_right x.ikind x.v y.v } (* TODO check ikinds*)
let c_lognot = lift_logical I.c_lognot
let c_logand = lift2 I.c_logand
let c_logor = lift2 I.c_logor

let cast_to ?(suppress_ovwarn=false) ~kind ikind x = {v = I.cast_to ~suppress_ovwarn ~kind ~from_ik:x.ikind ikind x.v; ikind}

Expand Down Expand Up @@ -631,9 +626,6 @@ struct
let logxor = Ints_t.logxor
let shift_left n1 n2 = Ints_t.shift_left n1 (Ints_t.to_int n2)
let shift_right n1 n2 = Ints_t.shift_right n1 (Ints_t.to_int n2)
let c_lognot n1 = of_bool (not (to_bool' n1))
let c_logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2))
let c_logor n1 n2 = of_bool ((to_bool' n1) || (to_bool' n2))
let cast_to ?(suppress_ovwarn=false) ~kind t x = failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "."
let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 (* TODO: use ikind *)
let invariant _ _ = Invariant.none (* TODO *)
Expand Down Expand Up @@ -728,9 +720,6 @@ struct
let logxor = lift2 Base.logxor
let shift_left = lift2 Base.shift_left
let shift_right = lift2 Base.shift_right
let c_lognot = lift1 Base.c_lognot
let c_logand = lift2 Base.c_logand
let c_logor = lift2 Base.c_logor

let invariant e = function
| `Lifted x -> Base.invariant e x
Expand Down Expand Up @@ -799,9 +788,6 @@ struct
let logxor = lift2 Base.logxor
let shift_left = lift2 Base.shift_left
let shift_right = lift2 Base.shift_right
let c_lognot = lift1 Base.c_lognot
let c_logand = lift2 Base.c_logand
let c_logor = lift2 Base.c_logor

let invariant e = function
| `Lifted x -> Base.invariant e x
Expand Down
26 changes: 0 additions & 26 deletions src/cdomain/value/cdomains/intDomain_intf.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,19 +67,6 @@ sig

val shift_right: t -> t -> t
(** Shifting bits right: [x >> y] *)


(** {b Logical operators} *)

val c_lognot: t -> t
(** Logical not: [!x] *)

val c_logand: t -> t -> t
(** Logical and: [x && y] *)

val c_logor : t -> t -> t
(** Logical or: [x || y] *)

end

module type ArithIkind =
Expand Down Expand Up @@ -146,19 +133,6 @@ sig

val shift_right: Cil.ikind -> t -> t -> t
(** Shifting bits right: [x >> y] *)


(** {b Logical operators} *)

val c_lognot: Cil.ikind -> t -> t
(** Logical not: [!x] *)

val c_logand: Cil.ikind -> t -> t -> t
(** Logical and: [x && y] *)

val c_logor : Cil.ikind -> t -> t -> t
(** Logical or: [x || y] *)

end

(* Shared signature of IntDomain implementations and the lifted IntDomains *)
Expand Down
15 changes: 0 additions & 15 deletions src/domains/intDomainProperties.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,9 +62,6 @@ struct
let logxor = logxor (Ik.ikind ())
let shift_left = shift_left (Ik.ikind ())
let shift_right = shift_right (Ik.ikind ())
let c_lognot = c_lognot (Ik.ikind ())
let c_logand = c_logand (Ik.ikind ())
let c_logor = c_logor (Ik.ikind ())

let of_int = of_int (Ik.ikind ())
let of_bool = of_bool (Ik.ikind ())
Expand Down Expand Up @@ -127,10 +124,6 @@ struct
let logxor = lift2 Base.logxor
let shift_left = lift2 Base.shift_left
let shift_right = lift2 Base.shift_right

let c_lognot = lift1 Base.c_lognot
let c_logand = lift2 Base.c_logand
let c_logor = lift2 Base.c_logor
end


Expand Down Expand Up @@ -182,10 +175,6 @@ struct
let valid_shift_left = make_valid2 ~name:"shift_left" ~cond:shift_cond CD.shift_left AD.shift_left
let valid_shift_right = make_valid2 ~name:"shift_right" ~cond:shift_cond CD.shift_right AD.shift_right

let valid_c_lognot = make_valid1 ~name:"c_lognot" ~cond:not_bot CD.c_lognot AD.c_lognot
let valid_c_logand = make_valid2 ~name:"c_logand" ~cond:none_bot CD.c_logand AD.c_logand
let valid_c_logor = make_valid2 ~name:"c_logor" ~cond:none_bot CD.c_logor AD.c_logor

let tests = [
valid_neg;
valid_add;
Expand All @@ -207,10 +196,6 @@ struct
valid_logxor;
valid_shift_left;
valid_shift_right;

valid_c_lognot;
valid_c_logand;
valid_c_logor
]
end

Expand Down
Loading