diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 440a1fcd96..caa718a616 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -174,7 +174,7 @@ struct let unop_ID = function | Neg -> ID.neg | BNot -> ID.bitnot - | LNot -> ID.lognot + | LNot -> ID.c_lognot let unop_FD = function | Neg -> FD.neg @@ -217,8 +217,8 @@ struct | BXor -> ID.bitxor | Shiftlt -> ID.shift_left | Shiftrt -> ID.shift_right - | LAnd -> ID.logand - | LOr -> ID.logor + | LAnd -> ID.c_logand + | LOr -> ID.c_logor | b -> (fun x y -> (ID.top_of result_ik)) let binop_FD (result_fk: Cil.fkind) = function @@ -2436,7 +2436,7 @@ struct | Isgreaterequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.ge x y)) | Isless (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.lt x y)) | Islessequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.le x y)) - | Islessgreater (x,y) -> Int(ID.logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y))) + | Islessgreater (x,y) -> Int(ID.c_logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y))) | Isunordered (x,y) -> Int(ID.cast_to IInt (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) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index efd098d994..6634b3f21c 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -44,7 +44,7 @@ struct let unop_ID = function | Neg -> ID.neg | BNot -> ID.bitnot - | LNot -> ID.lognot + | LNot -> ID.c_lognot let unop_FD = function | Neg -> FD.neg diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 46c43f44dd..e192e1341a 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -122,9 +122,9 @@ sig val shift_left : t -> t -> t val shift_right: t -> t -> t - val lognot: t -> t - val logand: t -> t -> t - val logor : t -> t -> t + val c_lognot: t -> t + val c_logand: t -> t -> t + val c_logor : t -> t -> t end @@ -153,9 +153,9 @@ sig val shift_left : Cil.ikind -> t -> t -> t val shift_right: Cil.ikind -> t -> t -> t - val lognot: Cil.ikind -> t -> t - val logand: Cil.ikind -> t -> t -> t - val logor : Cil.ikind -> t -> t -> t + val c_lognot: Cil.ikind -> t -> t + val c_logand: Cil.ikind -> t -> t -> t + val c_logor : Cil.ikind -> t -> t -> t end @@ -359,9 +359,9 @@ struct let bitxor = lift2 I.bitxor 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 lognot = lift_logical I.lognot - let logand = lift2 I.logand - let logor = lift2 I.logor + 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 ?torg ikind x = {v = I.cast_to ~torg:(TInt(x.ikind,[])) ikind x.v; ikind} @@ -703,8 +703,8 @@ struct | Some x, Some y -> of_bool ik (f x y) | _ -> top_of ik - let logor = log (||) ~annihilator:true - let logand = log (&&) ~annihilator:false + let c_logor = log (||) ~annihilator:true + let c_logand = log (&&) ~annihilator:false let log1 f ik i1 = if is_bot i1 then @@ -714,7 +714,7 @@ struct | Some x -> of_bool ik (f ik x) | _ -> top_of ik - let lognot = log1 (fun _ik -> not) + let c_lognot = log1 (fun _ik -> not) let bit f ik i1 i2 = match is_bot i1, is_bot i2 with @@ -1298,7 +1298,7 @@ struct let interval_shiftright = bitcomp (fun x y -> Ints_t.shift_right x (Ints_t.to_int y)) ik in binary_op_with_ovc x y interval_shiftright - let lognot ik x = + let c_lognot ik x = let log1 f ik i1 = match interval_to_bool i1 with | Some x -> of_bool ik (f x) @@ -1307,11 +1307,11 @@ struct let interval_lognot = log1 not ik in unop x interval_lognot - let logand ik x y = + let c_logand ik x y = let interval_logand = log (&&) ik in binop x y interval_logand - let logor ik x y = + let c_logor ik x y = let interval_logor = log (||) ik in binop x y interval_logor @@ -1597,9 +1597,9 @@ struct let bitxor = Ints_t.bitxor 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 lognot n1 = of_bool (not (to_bool' n1)) - let logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2)) - let logor n1 n2 = of_bool ((to_bool' n1) || (to_bool' 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 ?torg 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 *) @@ -1688,9 +1688,9 @@ struct let bitxor = lift2 Base.bitxor let shift_left = lift2 Base.shift_left let shift_right = lift2 Base.shift_right - let lognot = lift1 Base.lognot - let logand = lift2 Base.logand - let logor = lift2 Base.logor + 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 @@ -1755,9 +1755,9 @@ struct let bitxor = lift2 Base.bitxor let shift_left = lift2 Base.shift_left let shift_right = lift2 Base.shift_right - let lognot = lift1 Base.lognot - let logand = lift2 Base.logand - let logor = lift2 Base.logor + 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 @@ -2246,21 +2246,21 @@ struct let shift_right = shift Z.shift_right (* TODO: lift does not treat Not {0} as true. *) - let logand ik x y = + 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.logand ik x y - let logor ik x y = + 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.logor ik x y - let lognot ik = eq ik (of_int ik Z.zero) + lift2 IntOps.BigIntOps.c_logor ik x y + let c_lognot ik = eq ik (of_int ik Z.zero) let invariant_ikind e ik (x:t) = match x with @@ -2366,9 +2366,9 @@ struct let bitxor x y = x && not y || not x && y let shift_left n1 n2 = n1 let shift_right n1 n2 = n1 - let lognot = (not) - let logand = (&&) - let logor = (||) + let c_lognot = (not) + let c_logand = (&&) + let c_logor = (||) let arbitrary () = QCheck.bool let invariant _ _ = Invariant.none (* TODO *) end @@ -2617,7 +2617,7 @@ module Enums : S with type int_t = Z.t = struct let starting ?(suppress_ovwarn=false) ikind x = top_of ikind let ending ?(suppress_ovwarn=false) ikind x = top_of ikind - let lognot ik x = + let c_lognot ik x = if is_bot x then x else @@ -2625,8 +2625,8 @@ module Enums : S with type int_t = Z.t = struct | Some b -> of_bool ik (not b) | None -> top_bool - let logand = lift2 IntOps.BigIntOps.logand - let logor = lift2 IntOps.BigIntOps.logor + 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) -> @@ -2680,7 +2680,7 @@ module Enums : S with type int_t = Z.t = struct else top_bool) - let ne ik x y = lognot ik (eq ik x y) + let ne ik x y = c_lognot ik (eq ik x y) let invariant_ikind e ik x = match x with @@ -2929,8 +2929,8 @@ struct | Some x, Some y -> of_bool ik (f x y) | _ -> top_of ik - let logor = log (||) - let logand = log (&&) + let c_logor = log (||) + let c_logand = log (&&) let log1 f ik i1 = if is_bot i1 then @@ -2940,7 +2940,7 @@ struct | Some x -> of_bool ik (f ik x) | _ -> top_of ik - let lognot = log1 (fun _ik -> not) + let c_lognot = log1 (fun _ik -> not) let shift_right _ _ _ = top() @@ -3563,8 +3563,8 @@ module IntDomTupleImpl = struct let bitnot ik = map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.bitnot ik)} - 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 ?torg ?no_ov t = mapovc ~cast:true t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ?torg ?no_ov t)} @@ -3689,11 +3689,11 @@ module IntDomTupleImpl = struct let shift_right ik = map2ovc ik {f2_ovc= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.shift_right ik)} - let logand ik = - map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.logand 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 logor ik = - map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.logor 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 *) diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli index 35ebc03794..ebbf8ceaf3 100644 --- a/src/cdomain/value/cdomains/intDomain.mli +++ b/src/cdomain/value/cdomains/intDomain.mli @@ -77,13 +77,13 @@ sig (** {b Logical operators} *) - val lognot: t -> t + val c_lognot: t -> t (** Logical not: [!x] *) - val logand: t -> t -> t + val c_logand: t -> t -> t (** Logical and: [x && y] *) - val logor : t -> t -> t + val c_logor : t -> t -> t (** Logical or: [x || y] *) end @@ -156,13 +156,13 @@ sig (** {b Logical operators} *) - val lognot: Cil.ikind -> t -> t + val c_lognot: Cil.ikind -> t -> t (** Logical not: [!x] *) - val logand: Cil.ikind -> t -> t -> t + val c_logand: Cil.ikind -> t -> t -> t (** Logical and: [x && y] *) - val logor : Cil.ikind -> t -> t -> t + val c_logor : Cil.ikind -> t -> t -> t (** Logical or: [x || y] *) end diff --git a/src/common/util/intOps.ml b/src/common/util/intOps.ml index a14305b0c2..17df714a82 100644 --- a/src/common/util/intOps.ml +++ b/src/common/util/intOps.ml @@ -62,12 +62,12 @@ end module type IntOps = sig include IntOpsBase - (* Logical: These are intended to be the logical operations in the C sense! *) - (* Int64 calls its bit-wise operations e.g. logand, we call those e.g. bitand *) - val logand : t -> t -> t - val logor : t -> t -> t - val logxor : t -> t -> t - val lognot : t -> t + (* Logical: These are intended to be the logical operations in the C sense! *) + (* Int64 calls its bit-wise operations e.g. logand, without the c_ prefix *) + val c_logand : t -> t -> t + val c_logor : t -> t -> t + val c_logxor : t -> t -> t + val c_lognot : t -> t val to_bool : t -> bool val of_bool : bool -> t end @@ -281,10 +281,10 @@ struct (* These are logical operations in the C sense! *) let log_op op a b = of_bool @@ op (to_bool a) (to_bool b) - let lognot x = of_bool (x = zero) - let logand = log_op (&&) - let logor = log_op (||) - let logxor = log_op (<>) + let c_lognot x = of_bool (x = zero) + let c_logand = log_op (&&) + let c_logor = log_op (||) + let c_logxor = log_op (<>) let lt x y = of_bool (compare x y < 0) let gt x y = of_bool (compare x y > 0) diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml index e18ce65554..fcff746936 100644 --- a/src/domains/intDomainProperties.ml +++ b/src/domains/intDomainProperties.ml @@ -51,9 +51,9 @@ struct let bitxor = bitxor (Ik.ikind ()) let shift_left = shift_left (Ik.ikind ()) let shift_right = shift_right (Ik.ikind ()) - let lognot = lognot (Ik.ikind ()) - let logand = logand (Ik.ikind ()) - let logor = logor (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 ()) @@ -104,9 +104,9 @@ struct let shift_left = lift2 Base.shift_left let shift_right = lift2 Base.shift_right - let lognot = lift1 Base.lognot - let logand = lift2 Base.logand - let logor = lift2 Base.logor + let c_lognot = lift1 Base.c_lognot + let c_logand = lift2 Base.c_logand + let c_logor = lift2 Base.c_logor end @@ -145,9 +145,9 @@ 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_lognot = make_valid1 ~name:"lognot" ~cond:not_bot CD.lognot AD.lognot - let valid_logand = make_valid2 ~name:"logand" ~cond:none_bot CD.logand AD.logand - let valid_logor = make_valid2 ~name:"logor" ~cond:none_bot CD.logor AD.logor + let valid_lognot = make_valid1 ~name:"lognot" ~cond:not_bot CD.c_lognot AD.c_lognot + let valid_logand = make_valid2 ~name:"logand" ~cond:none_bot CD.c_logand AD.c_logand + let valid_logor = make_valid2 ~name:"logor" ~cond:none_bot CD.c_logor AD.c_logor let tests = [ valid_neg;