pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Obtain bitwidth and type from same arg of binop exps

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D12854509

fbshipit-source-id: 4d5504adb
master
Josh Berdine 6 years ago committed by Facebook Github Bot
parent 42fefadc38
commit 2a70b36140
1 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File

16
sledge/src/llair/exp.ml
Unescape View File

@ -620,7 +620,7 @@ and simp_dq x y =
and simp_and x y = and simp_and x y =
match (x, y) with match (x, y) with
(* i && j *) (* i && j *)
| Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} -> | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} ->
integer (Z.logand ~bits i j) typ integer (Z.logand ~bits i j) typ
(* e && true ==> e *) (* e && true ==> e *)
| Integer {data; typ= Integer {bits= 1}}, e | Integer {data; typ= Integer {bits= 1}}, e
@ -642,7 +642,7 @@ and simp_and x y =
and simp_or x y = and simp_or x y =
match (x, y) with match (x, y) with
(* i || j *) (* i || j *)
| Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} -> | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} ->
integer (Z.logor ~bits i j) typ integer (Z.logor ~bits i j) typ
(* e || true ==> true *) (* e || true ==> true *)
| (Integer {data; typ= Integer {bits= 1}} as t), _ | (Integer {data; typ= Integer {bits= 1}} as t), _
@ -664,7 +664,7 @@ and simp_or x y =
let simp_xor x y = let simp_xor x y =
match (x, y) with match (x, y) with
(* i xor j *) (* i xor j *)
| Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} -> | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} ->
integer (Z.logxor ~bits i j) typ integer (Z.logxor ~bits i j) typ
(* true xor b ==> ¬b *) (* true xor b ==> ¬b *)
| Integer {data; typ= Integer {bits= 1}}, b | Integer {data; typ= Integer {bits= 1}}, b
@ -679,7 +679,7 @@ let simp_xor x y =
let simp_shl x y = let simp_shl x y =
match (x, y) with match (x, y) with
(* i shl j *) (* i shl j *)
| Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
when Z.fits_int j -> when Z.fits_int j ->
integer (Z.shift_left ~bits i (Z.to_int j)) typ integer (Z.shift_left ~bits i (Z.to_int j)) typ
(* e shl 0 ==> e *) (* e shl 0 ==> e *)
@ -689,7 +689,7 @@ let simp_shl x y =
let simp_lshr x y = let simp_lshr x y =
match (x, y) with match (x, y) with
(* i lshr j *) (* i lshr j *)
| Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
when Z.fits_int j -> when Z.fits_int j ->
integer (Z.shift_right_trunc ~bits i (Z.to_int j)) typ integer (Z.shift_right_trunc ~bits i (Z.to_int j)) typ
(* e lshr 0 ==> e *) (* e lshr 0 ==> e *)
@ -699,7 +699,7 @@ let simp_lshr x y =
let simp_ashr x y = let simp_ashr x y =
match (x, y) with match (x, y) with
(* i ashr j *) (* i ashr j *)
| Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
when Z.fits_int j -> when Z.fits_int j ->
integer (Z.shift_right ~bits i (Z.to_int j)) typ integer (Z.shift_right ~bits i (Z.to_int j)) typ
(* e ashr 0 ==> e *) (* e ashr 0 ==> e *)
@ -752,7 +752,7 @@ let simp_sub typ x y =
let simp_div x y = let simp_div x y =
match (x, y) with match (x, y) with
(* i / j *) (* i / j *)
| Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} -> | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} ->
integer (Z.div ~bits i j) typ integer (Z.div ~bits i j) typ
(* e / 1 ==> e *) (* e / 1 ==> e *)
| Integer {data}, e when Z.equal Z.one data -> e | Integer {data}, e when Z.equal Z.one data -> e
@ -770,7 +770,7 @@ let simp_udiv x y =
let simp_rem x y = let simp_rem x y =
match (x, y) with match (x, y) with
(* i % j *) (* i % j *)
| Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} -> | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} ->
integer (Z.rem ~bits i j) typ integer (Z.rem ~bits i j) typ
(* e % 1 ==> 0 *) (* e % 1 ==> 0 *)
| _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ | _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ

Write Preview
Loading…
Cancel
Save