|
|
|
@ -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
|
|
|
|
|