From fd9f0e8101d6f32bc46859661d91966f335c028b Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 31 Oct 2018 03:57:26 -0700 Subject: [PATCH] IntLit: more types Reviewed By: skcho Differential Revision: D12839149 fbshipit-source-id: 31bd799b9 --- infer/src/IR/IntLit.ml | 113 ++++++++++++++++++++++------------------- 1 file changed, 60 insertions(+), 53 deletions(-) diff --git a/infer/src/IR/IntLit.ml b/infer/src/IR/IntLit.ml index 01fccc957..bb5297ac6 100644 --- a/infer/src/IR/IntLit.ml +++ b/infer/src/IR/IntLit.ml @@ -9,36 +9,45 @@ open! IStd module F = Format module L = Logging -(** signed and unsigned integer literals *) -type t = bool * Z.t * bool +type signedness = Signed | Unsigned [@@deriving compare] -exception OversizedShift +let join_signedness signedness1 signedness2 = + match (signedness1, signedness2) with Signed, Signed -> Signed | _ -> Unsigned -(* the first bool indicates whether this is an unsigned value, - and the second whether it is a pointer *) -let area u i = - match (Z.(i < zero), u) with - | true, false -> - (* only representable as signed *) 1 - | false, _ -> - (* in the intersection between signed and unsigned *) 2 - | true, true -> - (* only representable as unsigned *) 3 +type pointerness = NotPointer | Pointer +let join_pointerness pointerness1 pointerness2 = + match (pointerness1, pointerness2) with NotPointer, NotPointer -> NotPointer | _ -> Pointer -let to_signed (unsigned, i, ptr) = - if Int.equal (area unsigned i) 3 then None - else (* not representable as signed *) Some (false, i, ptr) +let compare_pointerness _ _ = 0 -let compare (unsigned1, i1, _) (unsigned2, i2, _) = - let n = Bool.compare unsigned1 unsigned2 in - if n <> 0 then n else Z.compare i1 i2 +(** signed and unsigned integer literals *) +type t = {signedness: signedness; i: Z.t; pointerness: pointerness} [@@deriving compare] +exception OversizedShift -let compare_value (unsigned1, i1, _) (unsigned2, i2, _) = - [%compare: int * Z.t] (area unsigned1 i1, i1) (area unsigned2 i2, i2) +let area {signedness; i} = + match (Z.(i < zero), signedness) with + | true, Signed -> + (* negative signed *) 1 + | false, _ -> + (* non-negative *) 2 + | true, Unsigned -> + (* negative unsigned *) 3 + + +let to_signed intlit = + match intlit with + | {signedness= Signed} -> + Some intlit + | {signedness= Unsigned; i} -> + if Z.(i < zero) then None else Some {intlit with signedness= Signed} + + +let compare_value intlit1 intlit2 = + [%compare: int * Z.t] (area intlit1, intlit1.i) (area intlit2, intlit2.i) let eq i1 i2 = Int.equal (compare_value i1 i2) 0 @@ -53,7 +62,7 @@ let geq i1 i2 = compare_value i1 i2 >= 0 let gt i1 i2 = compare_value i1 i2 > 0 -let of_z z_of_int i = (false, z_of_int i, false) +let of_z z_of_int i = {signedness= Signed; i= z_of_int i; pointerness= NotPointer} let of_int64 = of_z Z.of_int64 @@ -65,15 +74,15 @@ let of_string = of_z Z.of_string let z_to_int_opt i = try Some (Z.to_int i) with Z.Overflow -> None -let to_int (_, i, _) = z_to_int_opt i +let to_int {i} = z_to_int_opt i -let to_int_exn (_, i, _) = Z.to_int i +let to_int_exn {i} = Z.to_int i -let to_big_int (_, i, _) = i +let to_big_int {i} = i -let to_float (_, i, _) = Z.to_float i +let to_float {i} = Z.to_float i -let null = (false, Z.zero, true) +let null = {signedness= Signed; i= Z.zero; pointerness= Pointer} let zero = of_int 0 @@ -83,64 +92,62 @@ let two = of_int 2 let minus_one = of_int (-1) -let isone (_, i, _) = Z.(equal i one) +let isone {i} = Z.(equal i one) -let iszero (_, i, _) = Z.(equal i zero) +let iszero {i} = Z.(equal i zero) -let isnull (_, i, ptr) = Z.(equal i zero) && ptr +let isnull = function {pointerness= Pointer; i} when Z.(equal i zero) -> true | _ -> false -let isminusone (unsigned, i, _) = (not unsigned) && Z.(equal i minus_one) +let isminusone = function {signedness= Signed; i} when Z.(equal i minus_one) -> true | _ -> false -let isnegative (unsigned, i, _) = (not unsigned) && Z.(lt i zero) +let isnegative = function {signedness= Signed; i} when Z.(lt i zero) -> true | _ -> false -let neg (unsigned, i, ptr) = (unsigned, Z.neg i, ptr) +let lift2 binop intlit1 intlit2 = + { signedness= join_signedness intlit1.signedness intlit2.signedness + ; i= binop intlit1.i intlit2.i + ; pointerness= join_pointerness intlit1.pointerness intlit2.pointerness } -let lift binop (unsigned1, i1, ptr1) (unsigned2, i2, ptr2) = - (unsigned1 || unsigned2, binop i1 i2, ptr1 || ptr2) +let lift1 unop intlit = {intlit with i= unop intlit.i} -let lift1 unop (unsigned, i, ptr) = (unsigned, unop i, ptr) +let neg i = lift1 Z.neg i -let add i1 i2 = lift Z.( + ) i1 i2 +let add i1 i2 = lift2 Z.( + ) i1 i2 -let mul i1 i2 = lift Z.( * ) i1 i2 +let mul i1 i2 = lift2 Z.( * ) i1 i2 -let div i1 i2 = lift Z.( / ) i1 i2 +let div i1 i2 = lift2 Z.( / ) i1 i2 -let rem i1 i2 = lift Z.rem i1 i2 +let rem i1 i2 = lift2 Z.rem i1 i2 -let logand i1 i2 = lift Z.logand i1 i2 +let logand i1 i2 = lift2 Z.logand i1 i2 -let logor i1 i2 = lift Z.logor i1 i2 +let logor i1 i2 = lift2 Z.logor i1 i2 -let logxor i1 i2 = lift Z.logxor i1 i2 +let logxor i1 i2 = lift2 Z.logxor i1 i2 let lognot i = lift1 Z.lognot i -let sub i1 i2 = add i1 (neg i2) +let sub i1 i2 = lift2 Z.( - ) i1 i2 -let shift_left (unsigned1, i1, ptr1) (_, i2, _) = +let shift_left intlit1 {i= i2} = match z_to_int_opt i2 with | None -> L.(die InternalError) "Shifting failed with operand %a" Z.pp_print i2 | Some i2 -> if i2 < 0 || i2 >= 64 then raise OversizedShift ; - let res = Z.shift_left i1 i2 in - (unsigned1, res, ptr1) + lift1 (fun i -> Z.shift_left i i2) intlit1 -let shift_right (unsigned1, i1, ptr1) (_, i2, _) = +let shift_right intlit1 {i= i2} = match z_to_int_opt i2 with | None -> L.(die InternalError) "Shifting failed with operand %a" Z.pp_print i2 | Some i2 -> if i2 < 0 || i2 >= 64 then raise OversizedShift ; - let res = Z.shift_right i1 i2 in - (unsigned1, res, ptr1) - + lift1 (fun i -> Z.shift_right i i2) intlit1 -let pp f (_, n, ptr) = - if ptr && Z.(equal n zero) then F.pp_print_string f "null" else Z.pp_print f n +let pp f intlit = if isnull intlit then F.pp_print_string f "null" else Z.pp_print f intlit.i let to_string i = F.asprintf "%a" pp i