Skip to content

Commit

Permalink
Merge pull request #1505 from goblint/option-get-simplifications
Browse files Browse the repository at this point in the history 
Simplify some `Option.get` usages
  • Loading branch information
@sim642
sim642 authored Jun 13, 2024
2 parents 60ecfe7 + ae12610 commit b016c54
Show file tree
Hide file tree
Showing 5 changed files with 31 additions and 31 deletions.
4 changes: 2 additions & 2 deletions src/cdomain/value/cdomains/floatDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -241,12 +241,12 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct

let minimal = function
| Bot -> raise (ArithmeticOnFloatBot (Printf.sprintf "minimal %s" (show Bot)))
| Interval (l, _) -> Float_t.to_float l
| Interval (l, _) -> Some (Float_t.to_float l)
| _ -> None

let maximal = function
| Bot -> raise (ArithmeticOnFloatBot (Printf.sprintf "maximal %s" (show Bot)))
| Interval (_, h) -> Float_t.to_float h
| Interval (_, h) -> Some (Float_t.to_float h)
| _ -> None

let is_exact = function
Expand Down
22 changes: 11 additions & 11 deletions src/cdomain/value/cdomains/intDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2266,9 +2266,8 @@ struct
shift_op a b
in
(* If one of the parameters of the shift is negative, the result is undefined *)
let x_min = minimal x in
let y_min = minimal y in
if x_min = None || y_min = None || Z.compare (Option.get x_min) Z.zero < 0 || Z.compare (Option.get y_min) Z.zero < 0 then
let is_negative = GobOption.for_all (fun x -> Z.lt x Z.zero) in
if is_negative (minimal x) || is_negative (minimal y) then
top_of ik
else
norm ik @@ lift2 shift_op_big_int ik x y
Expand Down Expand Up @@ -2414,7 +2413,6 @@ module Booleans = MakeBooleans (

(* Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions. *)
module Enums : S with type int_t = Z.t = struct
open Batteries
module R = Interval32 (* range for exclusion *)

let range_ikind = Cil.IInt
Expand Down Expand Up @@ -2524,21 +2522,23 @@ module Enums : S with type int_t = Z.t = struct
let ex = if Z.gt x Z.zero || Z.lt y Z.zero then BISet.singleton Z.zero else BISet.empty () in
norm ik @@ (Exc (ex, r))

let join ik = curry @@ function
let join _ x y =
match x, y with
| Inc x, Inc y -> Inc (BISet.union x y)
| Exc (x,r1), Exc (y,r2) -> Exc (BISet.inter x y, R.join r1 r2)
| Exc (x,r), Inc y
| Inc y, Exc (x,r) ->
let r = if BISet.is_empty y
then r
else
let (min_el_range, max_el_range) = Tuple2.mapn (fun x -> R.of_interval range_ikind (Size.min_range_sign_agnostic x)) (BISet.min_elt y, BISet.max_elt y) in
let (min_el_range, max_el_range) = Batteries.Tuple2.mapn (fun x -> R.of_interval range_ikind (Size.min_range_sign_agnostic x)) (BISet.min_elt y, BISet.max_elt y) in
let range = R.join min_el_range max_el_range in
R.join r range
in
Exc (BISet.diff x y, r)

let meet ikind = curry @@ function
let meet _ x y =
match x, y with
| Inc x, Inc y -> Inc (BISet.inter x y)
| Exc (x,r1), Exc (y,r2) ->
let r = R.meet r1 r2 in
Expand Down Expand Up @@ -2592,7 +2592,8 @@ module Enums : S with type int_t = Z.t = struct
try lift2 f ikind a b with Division_by_zero -> top_of ikind

let neg ?no_ov = lift1 Z.neg
let add ?no_ov ikind = curry @@ function
let add ?no_ov ikind a b =
match a, b with
| Inc z,x when BISet.is_singleton z && BISet.choose z = Z.zero -> x
| x,Inc z when BISet.is_singleton z && BISet.choose z = Z.zero -> x
| x,y -> lift2 Z.add ikind x y
Expand Down Expand Up @@ -2626,9 +2627,8 @@ module Enums : S with type int_t = Z.t = struct
shift_op a b
in
(* If one of the parameters of the shift is negative, the result is undefined *)
let x_min = minimal x in
let y_min = minimal y in
if x_min = None || y_min = None || Z.compare (Option.get x_min) Z.zero < 0 || Z.compare (Option.get y_min) Z.zero < 0 then
let is_negative = GobOption.for_all (fun x -> Z.lt x Z.zero) in
if is_negative (minimal x) || is_negative (minimal y) then
top_of ik
else
lift2 shift_op_big_int ik x y)
Expand Down
6 changes: 3 additions & 3 deletions src/common/cdomains/floatOps/floatOps.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ module type CFloatType = sig
val pi : t

val of_float: round_mode -> float -> t
val to_float: t -> float option
val to_float: t -> float
val to_big_int: t -> Z.t

val is_finite: t -> bool
Expand Down Expand Up @@ -68,7 +68,7 @@ module CDouble = struct
let pi = Float.pi

let of_float _ x = x
let to_float x = Some x
let to_float x = x
let to_big_int = big_int_of_float

let is_finite = Float.is_finite
Expand Down Expand Up @@ -112,7 +112,7 @@ module CFloat = struct
let smallest = smallest' ()
let pi = pi' ()

let to_float x = Some x
let to_float x = x
let to_big_int = big_int_of_float

let is_finite x = Float.is_finite x && x >= lower_bound && x <= upper_bound
Expand Down
2 changes: 1 addition & 1 deletion src/common/cdomains/floatOps/floatOps.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ module type CFloatType = sig
val pi : t

val of_float: round_mode -> float -> t
val to_float: t -> float option
val to_float: t -> float
val to_big_int: t -> Z.t

val is_finite: t -> bool
Expand Down
28 changes: 14 additions & 14 deletions tests/unit/cdomains/floatDomainTest.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,12 @@ struct
let mul = Float_t.mul
let div = Float_t.div

let pred x = Option.get (to_float (Float_t.pred (of_float Nearest x)))
let succ x = Option.get (to_float (Float_t.succ (of_float Nearest x)))
let pred x = to_float (Float_t.pred (of_float Nearest x))
let succ x = to_float (Float_t.succ (of_float Nearest x))

let fmax = Option.get (to_float Float_t.upper_bound)
let fmin = Option.get (to_float Float_t.lower_bound)
let fsmall = Option.get (to_float Float_t.smallest)
let fmax = to_float Float_t.upper_bound
let fmin = to_float Float_t.lower_bound
let fsmall = to_float Float_t.smallest

let fi_zero = FI.of_const 0.
let fi_one = FI.of_const 1.
Expand Down Expand Up @@ -53,7 +53,7 @@ struct
FI.top () + FI.top () = FI.top ();
(FI.of_const fmin) + (FI.of_const fmax) = fi_zero;
(FI.of_const fsmall) + (FI.of_const fsmall) = FI.of_const (fsmall +. fsmall);
let one_plus_fsmall = Option.get (to_float (Float_t.add Up (Float_t.of_float Up 1.) Float_t.smallest)) in
let one_plus_fsmall = to_float (Float_t.add Up (Float_t.of_float Up 1.) Float_t.smallest) in
(FI.of_const fsmall) + (FI.of_const 1.) = FI.of_interval (1., one_plus_fsmall);
(FI.of_interval (1., 2.)) + (FI.of_interval (2., 3.)) = FI.of_interval (3., 5.);
(FI.of_interval (-. 2., 3.)) + (FI.of_interval (-. 100., 20.)) = FI.of_interval (-. 102., 23.);
Expand Down Expand Up @@ -286,27 +286,27 @@ struct
let test_FI_add =
QCheck.Test.make ~name:"test_FI_add" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) ->
let result = FI.add (FI.of_const arg1) (FI.of_const arg2) in
(FI.leq (FI.of_const (Option.get (to_float (add Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) &&
(FI.leq (FI.of_const (Option.get (to_float (add Down (of_float Nearest arg1) (of_float Nearest arg2))))) result))
(FI.leq (FI.of_const (to_float (add Up (of_float Nearest arg1) (of_float Nearest arg2)))) result) &&
(FI.leq (FI.of_const (to_float (add Down (of_float Nearest arg1) (of_float Nearest arg2)))) result))

let test_FI_sub =
QCheck.Test.make ~name:"test_FI_sub" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) ->
let result = FI.sub (FI.of_const arg1) (FI.of_const arg2) in
(FI.leq (FI.of_const (Option.get (to_float (sub Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) &&
(FI.leq (FI.of_const (Option.get (to_float (sub Down (of_float Nearest arg1) (of_float Nearest arg2))))) result))
(FI.leq (FI.of_const (to_float (sub Up (of_float Nearest arg1) (of_float Nearest arg2)))) result) &&
(FI.leq (FI.of_const (to_float (sub Down (of_float Nearest arg1) (of_float Nearest arg2))))) result)

let test_FI_mul =
QCheck.Test.make ~name:"test_FI_mul" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) ->
let result = FI.mul (FI.of_const arg1) (FI.of_const arg2) in
(FI.leq (FI.of_const (Option.get (to_float (mul Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) &&
(FI.leq (FI.of_const (Option.get (to_float (mul Down (of_float Nearest arg1) (of_float Nearest arg2))))) result))
(FI.leq (FI.of_const (to_float (mul Up (of_float Nearest arg1) (of_float Nearest arg2)))) result) &&
(FI.leq (FI.of_const (to_float (mul Down (of_float Nearest arg1) (of_float Nearest arg2)))) result))


let test_FI_div =
QCheck.Test.make ~name:"test_FI_div" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) ->
let result = FI.div (FI.of_const arg1) (FI.of_const arg2) in
(FI.leq (FI.of_const (Option.get (to_float (div Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) &&
(FI.leq (FI.of_const (Option.get (to_float (div Down (of_float Nearest arg1) (of_float Nearest arg2))))) result))
(FI.leq (FI.of_const (to_float (div Up (of_float Nearest arg1) (of_float Nearest arg2)))) result) &&
(FI.leq (FI.of_const (to_float (div Down (of_float Nearest arg1) (of_float Nearest arg2)))) result))


let test () = [
Expand Down

0 comments on commit b016c54

Please sign in to comment.